Theorems · Theorem · field theory
Irreducible.separable
∀ {F : Type u} [inst : Field F] [CharZero F] {f : Polynomial F}, Irreducible f → f.Separable- Defined in
- Mathlib.FieldTheory.Separable
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 124 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Fieldstatement and proof · cited by 7,404
- Polynomialstatement and proof · cited by 5,681
- Bot.botproof · cited by 4,720
- WithBotproof · cited by 1,498
- LT.lt.ne'proof · cited by 1,417
- Polynomial.natDegreeproof · cited by 1,105
- CharZerostatement and proof · cited by 932
- Irreduciblestatement and proof · cited by 496
- Polynomial.derivativeproof · cited by 331
- Polynomial.Separablestatement · cited by 117
- Polynomial.degree_eq_botproof · cited by 34
Cited by6
Results whose statement or proof uses this declaration.
- Irreducible.hasSeparableContractionproof · cited by 4
- PerfectRing.toPerfectFieldproof · cited by 2
- Polynomial.Gal.prime_degree_dvd_cardproof · cited by 1
- Polynomial.Gal.galActionHom_bijective_of_prime_degreeproof · cited by 1
- IsSeparable.of_integralproof · cited by 0
- IsAlgClosed.of_denseRangeproof · cited by 0