Theorems · Theorem · field theory
Polynomial.separable_iff_derivative_ne_zero
∀ {F : Type u} [inst : Field F] {f : Polynomial F}, Irreducible f → (f.Separable ↔ Polynomial.derivative f ≠ 0)- Defined in
- Mathlib.FieldTheory.Separable
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 123 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.
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
- RingHom.idstatement · cited by 18,349
- LinearMapstatement · cited by 10,215
- Fieldstatement and proof · cited by 7,404
- Polynomialstatement and proof · cited by 5,681
- Unitsproof · cited by 2,804
- Units.valproof · cited by 1,966
- IsUnitproof · cited by 1,602
- Irreduciblestatement and proof · cited by 496
- Polynomial.derivativestatement and proof · cited by 331
- Polynomial.Separablestatement and proof · cited by 117
- not_lt_of_geproof · cited by 52
Cited by2
Results whose statement or proof uses this declaration.
- Irreducible.separableproof · cited by 6
- Polynomial.separable_orproof · cited by 3