Polynomial

Results named in Tau Ceti's TauCeti.RingTheory.Polynomial modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremGauss's lemma at a nonarchimedean absolute value#

A primitive polynomial with integer coefficients has Gauss norm of radius one equal to 1 at every nonarchimedean absolute value, in any characteristic.

Polynomial.IsPrimitive.gaussNorm_map_eq_one.{u_1} {R : Type u_1} [Ring R] [Nontrivial R]
  {v : AbsoluteValue R ℝ} (hna : IsNonarchimedean ⇑v) {p : Polynomial ℤ} (hp : p.IsPrimitive) :
  Polynomial.gaussNorm v 1 (Polynomial.map (Int.castRingHom R) p) = 1

Lean

Formalized in Tau Ceti as Polynomial.IsPrimitive.gaussNorm_map_eq_one.

Sources

• Tau Ceti documentation: Polynomial.IsPrimitive.gaussNorm_map_eq_one
• Source of Polynomial.IsPrimitive.gaussNorm_map_eq_one in TauCeti/RingTheory/Polynomial/GaussNorm.lean

LeanPolynomial.IsPrimitive.gaussNorm_map_eq_one

Used by 1

Used byNorthcott's theorem for the naive height, with Evertse's count

TheoremStructure theorem for subresultants, degree gap#

For consecutive entries s, t of the signed remainder sequence of p and q after the first, the subresultants of p and q at the indices strictly between deg t and deg s - 1 vanish.

Polynomial.subresultant_eq_zero_of_getElem?_sturmSeq.{u_1} {K : Type u_1} [Field K] [DecidableEq K]
  {p q s t : Polynomial K} {m i j : ℕ} (hp : p.natDegree ≤ m) (hs : (p.sturmSeq q)[i + 1]? = some s)
  (ht : (p.sturmSeq q)[i + 2]? = some t) (htj : t.natDegree < j) (hjs : j + 1 < s.natDegree) :
  p.subresultant q m q.natDegree j = 0

Lean

Formalized in Tau Ceti as Polynomial.subresultant_eq_zero_of_getElem?_sturmSeq.

Other forms

Structure theorem for subresultants, lower index. Formalized in Tau Ceti as Polynomial.exists_subresultant_natDegree_eq_C_mul_of_getElem?_sturmSeq.

Polynomial.exists_subresultant_natDegree_eq_C_mul_of_getElem?_sturmSeq.{u_1} {K : Type u_1}
  [Field K] [DecidableEq K] {p q s t : Polynomial K} {m i : ℕ} (hp : p.natDegree ≤ m)
  (hq : i = 0 → q.natDegree ≤ m) (hs : (p.sturmSeq q)[i + 1]? = some s)
  (ht : (p.sturmSeq q)[i + 2]? = some t) :
  ∃ c, c ≠ 0 ∧ p.subresultant q m q.natDegree t.natDegree = Polynomial.C c * t

Structure theorem for subresultants, upper index. Formalized in Tau Ceti as Polynomial.exists_subresultant_natDegree_sub_one_eq_C_mul_of_getElem?_sturmSeq.

Polynomial.exists_subresultant_natDegree_sub_one_eq_C_mul_of_getElem?_sturmSeq.{u_1} {K : Type u_1}
  [Field K] [DecidableEq K] {p q s t : Polynomial K} {m i : ℕ} (hp : p.natDegree ≤ m)
  (hq : i = 0 → q.natDegree ≤ m) (hs : (p.sturmSeq q)[i + 1]? = some s)
  (ht : (p.sturmSeq q)[i + 2]? = some t) :
  ∃ c, c ≠ 0 ∧ p.subresultant q m q.natDegree (s.natDegree - 1) = Polynomial.C c * t

Sources

• Tau Ceti documentation: Polynomial.subresultant_eq_zero_of_getElem?_sturmSeq
• Source of Polynomial.subresultant_eq_zero_of_getElem?_sturmSeq in TauCeti/RingTheory/Polynomial/Subresultant/Structure.lean

LeanPolynomial.subresultant_eq_zero_of_getElem?_sturmSeq · Polynomial.exists_subresultant_natDegree_eq_C_mul_of_getElem?_sturmSeq · Polynomial.exists_subresultant_natDegree_sub_one_eq_C_mul_of_getElem?_sturmSeq

TheoremVieta's formulas on the symmetric power#

the k-th coefficient of the monic polynomial of an unordered n-tuple is the (n - k)-th elementary symmetric function of the tuple, up to the sign (-1) ^ (n - k).

TauCeti.Sym.coeff_toMonic.{u_1} {R : Type u_1} [CommRing R] {n : ℕ} [Nontrivial R] (s : Sym R n)
  {k : ℕ} (hk : k ≤ n) : (↑(TauCeti.Sym.toMonic s)).coeff k = (-1) ^ (n - k) * (↑s).esymm (n - k)

Lean

Formalized in Tau Ceti as TauCeti.Sym.coeff_toMonic.

Other forms

Vieta's formulas for an indexed family of roots. Formalized in Tau Ceti as MvPolynomial.aeval_esymm_eq_coeff_prod_X_sub_C.

MvPolynomial.aeval_esymm_eq_coeff_prod_X_sub_C.{u_1, u_2, u_3} {σ : Type u_1} {R : Type u_2}
  {S : Type u_3} [Fintype σ] [CommSemiring R] [CommRing S] [Algebra R S] (x : σ → S) {k : ℕ}
  (hk : k ≤ Fintype.card σ) :
  (MvPolynomial.aeval x) (MvPolynomial.esymm σ R k) =
    (-1) ^ k * (∏ i, (Polynomial.X - Polynomial.C (x i))).coeff (Fintype.card σ - k)

Vieta's formulas, read through a root enumeration. Formalized in Tau Ceti as Polynomial.IsRootEnumeration.aeval_esymm_eq_coeff.

Polynomial.IsRootEnumeration.aeval_esymm_eq_coeff.{u_1, u_2, u_4} {R : Type u_1} {L : Type u_2}
  {ι : Type u_4} [CommRing R] [CommRing L] [IsDomain L] [Algebra R L] [Fintype ι] {f : Polynomial R}
  {x : ι → L} (hx : f.IsRootEnumeration x) (hf : f.Monic) (hdeg : f.natDegree ≤ Fintype.card ι)
  {k : ℕ} (hk : k ≤ Fintype.card ι) :
  (MvPolynomial.aeval x) (MvPolynomial.esymm ι R k) =
    (-1) ^ k * (algebraMap R L) (f.coeff (Fintype.card ι - k))

Sources

• Tau Ceti documentation: TauCeti.Sym.coeff_toMonic
• Source of TauCeti.Sym.coeff_toMonic in TauCeti/RingTheory/Polynomial/SymmetricPower.lean

LeanTauCeti.Sym.coeff_toMonic · MvPolynomial.aeval_esymm_eq_coeff_prod_X_sub_C · Polynomial.IsRootEnumeration.aeval_esymm_eq_coeff

Used by 2

Used byThe symmetric power of a complex curve is a complex analytic manifold · Vieta's formulas, in the form the symmetric descent uses

TheoremThe Wronskian criterion#

Over a field of characteristic zero, a family of polynomials is linearly independent if and only if its Hasse Wronskian is nonzero.

Polynomial.linearIndependent_iff_hasseWronskian_ne_zero.{u_3} {m : ℕ} {K : Type u_3} [Field K]
  [CharZero K] {g : Fin m → Polynomial K} : LinearIndependent K g ↔ Polynomial.hasseWronskian g ≠ 0

Lean

Formalized in Tau Ceti as Polynomial.linearIndependent_iff_hasseWronskian_ne_zero.

Sources

• Tau Ceti documentation: Polynomial.linearIndependent_iff_hasseWronskian_ne_zero
• Source of Polynomial.linearIndependent_iff_hasseWronskian_ne_zero in TauCeti/RingTheory/Polynomial/HasseWronskian.lean

LeanPolynomial.linearIndependent_iff_hasseWronskian_ne_zero

Used by 1

Used byThue's gap principle (Evertse, Theorem 6.14)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.