Theorems · Definition · field theory
Polynomial.natSepDegree
{F : Type u} → [inst : Field F] → Polynomial F → ℕThe separable degree Polynomial.natSepDegree of a polynomial is a natural number,
defined to be the number of distinct roots of it over its splitting field.
This is similar to Polynomial.natDegree but not to Polynomial.degree, namely, the separable
degree of 0 is 0, not negative infinity.
- Defined in
- Mathlib.FieldTheory.SeparableDegree
- Cited by
- 53 results in Mathlib
- Foundations
- Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- Polynomialstatement and proof · cited by 5,681
- Finset.cardproof · cited by 2,327
- Multiset.toFinsetproof · cited by 230
- Polynomial.arootsproof · cited by 89
- Polynomial.SplittingFieldproof · cited by 42
Cited by53
Results whose statement or proof uses this declaration.
- isPurelyInseparable_iff_pow_memproof · cited by 10
- Polynomial.natSepDegree_eq_of_isAlgClosedstatement · cited by 9
- Polynomial.natSepDegree_zerostatement and proof · cited by 5
- Polynomial.natSepDegree_X_sub_Cstatement · cited by 4
- Polynomial.natSepDegree_expandstatement and proof · cited by 4
- Polynomial.natSepDegree_powstatement · cited by 4
- Polynomial.Separable.natSepDegree_eq_natDegreestatement · cited by 4
- minpoly.natSepDegree_eq_one_iff_pow_memstatement and proof · cited by 4
- IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iffproof · cited by 4
- Irreducible.natSepDegree_eq_one_iff_of_monic'statement and proof · cited by 3
- Polynomial.natSepDegree_X_pow_char_pow_sub_Cstatement and proof · cited by 3
- Polynomial.natSepDegree_eq_zero_iffstatement · cited by 3