Theorems · Theorem · field theory

MvPolynomial.isAlgebraic_of_mem_vars_of_forall_totalDegree_le

∀ {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) →
    (MvPolynomial.aeval a) F = 0 → ∀ i ∈ F.vars, IsAlgebraic (↥(Algebra.adjoin k (a '' {i}ᶜ))) (a i)

Defined in: Mathlib.FieldTheory.SeparablyGenerated
Cited by: 1 results in Mathlib
Foundations: Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Field Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites26

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement · cited by 53,352
Finsetstatement · cited by 13,712
Algebrastatement and proof · cited by 11,388
Fieldstatement and proof · cited by 7,404
Polynomialproof · cited by 5,681
Set.imagestatement and proof · cited by 5,609
Finsuppstatement and proof · cited by 5,255
AlgHomstatement · cited by 3,236
Compl.complstatement and proof · cited by 2,925
MvPolynomialstatement and proof · cited by 2,140
Subalgebrastatement · cited by 1,353

Cited by1

Results whose statement or proof uses this declaration.

exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_powproof · cited by 2