Theorems · Theorem · field theory

MvPolynomial.coeff_toPolynomialAdjoinImageCompl_ne_zero

∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {a : ι → K}
  {F : MvPolynomial ι k},
  (∀ (F' : MvPolynomial ι k), F' ≠ 0 → (MvPolynomial.aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree) →
    ∀ σ ∈ F.support, ∀ (i : ι), σ i ≠ 0 → (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) ≠ 0

Defined in

Mathlib.FieldTheory.SeparablyGenerated

Cited by

2 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebra