Theorems · Theorem · field theory

MvPolynomial.irreducible_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) →
    F ≠ 0 → (MvPolynomial.aeval a) F = 0 → Irreducible F

If F has minimal total degree among the relations of a, then F is irreducible.

Defined in: Mathlib.FieldTheory.SeparablyGenerated
Cited by: 1 results in Mathlib
Foundations: Depth 123 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.

Cites21

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
Algebrastatement and proof · cited by 11,388
Fieldstatement and proof · cited by 7,404
Finsuppstatement · cited by 5,255
AlgHomstatement · cited by 3,236
mul_commproof · cited by 2,262
MvPolynomialstatement and proof · cited by 2,140
IsUnitproof · cited by 1,602
map_mulproof · cited by 1,137
Irreduciblestatement · cited by 496
MvPolynomial.Cproof · cited by 400
MvPolynomial.aevalstatement and proof · cited by 298

Cited by1

Results whose statement or proof uses this declaration.

exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_powproof · cited by 2