Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersGuruswamiSudan.rootMultiplicity_ge_of_shift_zero
Plain-language statement
If the shifted polynomial has no non-zero coefficients of total degree less than m, then the root multiplicity is at least m.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.rootMultiplicity_le_of_coeff_ne_zero
Plain-language statement
If the (s, t)-coefficient of shift Q x y is non-zero, then the root multiplicity of Q at (x, y) is at most s + t.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.roots_le_degree_of_deg_lt_roots
Plain-language statement
If a polynomial R has roots at points indexed by A with multiplicity at least m, and its degree is strictly less than m * |A|, then R must be the zero polynomial.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.sufficient_multiplicity_bound
Plain-language statement
The degree bound is strictly less than m times the number of agreement points, provided the distance is within the Johnson radius.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.toPolynomial_degree_le
Plain-language statement
The polynomial corresponding to a codeword has degree at most k-1.
Source project: ArkLib
Person-level attribution pending.
Ideal.principal_is_maximal_iff_irred
Project documentation
A principal ideal is an ideal generated by a single element. -/ def principalIdeal {F : Type} [Semiring F] (f : F) : Ideal F := Ideal.span {f} /- A principal ideal in a polynomial ring is maximal if and only if its generator is an irreducble polynomial.
Source project: ArkLib
Person-level attribution pending.