Theorems · Theorem · field theory
Polynomial.nodup_roots_iff_of_splits
∀ {F : Type u} [inst : Field F] {f : Polynomial F}, f ≠ 0 → f.Splits → (f.roots.Nodup ↔ f.Separable)If a non-zero polynomial splits, then it has no repeated roots on that field if and only if it is separable.
- Defined in
- Mathlib.FieldTheory.Separable
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 141 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.
Cites20
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
- Polynomial.evalproof · cited by 796
- Polynomial.derivativeproof · cited by 331
- Polynomial.Splitsstatement and proof · cited by 290
- Polynomial.rootsstatement · cited by 264
- Multiset.Nodupstatement · cited by 148
- GCDMonoid.gcdproof · cited by 143
- Polynomial.Separablestatement and proof · cited by 117
- LT.lt.trans_eqproof · cited by 65
- GCDMonoid.gcd_dvd_leftproof · cited by 36
Cited by1
Results whose statement or proof uses this declaration.
- Polynomial.nodup_aroots_iff_of_splitsproof · cited by 1