feat(field_theory/separable): a separable polynomial is squarefree (#…

…5039)

I prove that a separable polynomial is squarefree.

src/field_theory/separable.lean

@@ -8,6 +8,7 @@ import algebra.polynomial.big_operators
 import field_theory.minimal_polynomial
 import field_theory.splitting_field
 import field_theory.tower
+import algebra.squarefree
 
 /-!
 
@@ -449,6 +450,15 @@ begin
   exact_mod_cast (enat.add_one_le_of_lt hq)
 end
 
+lemma separable.squarefree {p : polynomial F}  (hsep : separable p) : squarefree p :=
+begin
+  rw multiplicity.squarefree_iff_multiplicity_le_one p,
+  intro f,
+  by_cases hunit : is_unit f,
+  { exact or.inr hunit },
+  exact or.inl (multiplicity_le_one_of_separable hunit hsep)
+end
+
 lemma root_multiplicity_le_one_of_separable {p : polynomial F} (hp : p ≠ 0)
   (hsep : separable p) (x : F) : root_multiplicity x p ≤ 1 :=
 begin