Research proof index

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.

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.

The degree bound is strictly less than m times the number of agreement points, provided the distance is within the Johnson radius.

The polynomial corresponding to a codeword has degree at most k-1.

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.

inductively to each such matrix, we conclude that, for each r_{ϑ-1} ∈ R*, d^{2^{ϑ-1}}((1-r_{ϑ-1}) · U₀ + r_{ϑ-1} · U₁, C^{2^{ϑ-1}}) ≤ e -/ lemma correlatedAgreement_of_mem_R_star_tensor {ϑ_pred : ℕ} (ih : δ_ε_multilinearCorrelatedAgreement_Nat (F := F) (A := A) (ι := ι) (C := MC) (ϑ := ϑ_pred) (e := e) (ε := ε)) (u : Fin (2 ^ (ϑ_pred + 1)) → (Word A ι...