From 68adaba31d941ab0801317d993f81921667db0b3 Mon Sep 17 00:00:00 2001
From: Aaron Anderson <awainverse@gmail.com>
Date: Thu, 19 Nov 2020 01:49:36 +0000
Subject: [PATCH] chore(field_theory/separable): spell-check "seperable" to
 "separable" (#5040)

Replacing instances of "seperable" with "separable"
---
 src/field_theory/separable.lean | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 8e30edea7ffd7..a225991e038d3 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -216,7 +216,8 @@ by { rw [separable_def, derivative_mul], exact ((hf.mul_right h).add_mul_left_ri
   ((h.symm.mul_right hg).mul_add_right_right _) }
 
 lemma separable_prod' {ι : Sort*} {f : ι → polynomial R} {s : finset ι} :
-  (∀x∈s, ∀y∈s, x ≠ y → is_coprime (f x) (f y)) → (∀x∈s, (f x).separable) → (∏ x in s, f x).separable :=
+  (∀x∈s, ∀y∈s, x ≠ y → is_coprime (f x) (f y)) → (∀x∈s, (f x).separable) →
+  (∏ x in s, f x).separable :=
 finset.induction_on s (λ _ _, separable_one) $ λ a s has ih h1 h2, begin
   simp_rw [finset.forall_mem_insert, forall_and_distrib] at h1 h2, rw prod_insert has,
   exact h2.1.mul (ih h1.2.2 h2.2) (is_coprime.prod_right $ λ i his, h1.1.2 i his $
@@ -401,7 +402,8 @@ begin
     { rw is_unit_iff at h, rcases h with ⟨r, hr, rfl⟩,
       simp_rw expand_C at hf, exact absurd (is_unit_C.2 hr) hf.1 },
     { rw [add_zero, pow_zero, expand_one], split; refl } },
-  exact λ g₁ g₂ hg₁ hgf₁ hg₂ hgf₂, let ⟨hn, hg⟩ := this g₂ g₁ hg₂ hgf₂ hg₁ hgf₁ in ⟨hn.symm, hg.symm⟩
+  exact λ g₁ g₂ hg₁ hgf₁ hg₂ hgf₂, let ⟨hn, hg⟩ :=
+    this g₂ g₁ hg₂ hgf₂ hg₁ hgf₁ in ⟨hn.symm, hg.symm⟩
 end
 
 end char_p
@@ -437,7 +439,7 @@ begin
   simpa only [multiset.map_cons, multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)
 end
 
-lemma multiplicity_le_one_of_seperable {p q : polynomial F} (hq : ¬ is_unit q)
+lemma multiplicity_le_one_of_separable {p q : polynomial F} (hq : ¬ is_unit q)
   (hsep : separable p) : multiplicity q p ≤ 1 :=
 begin
   contrapose! hq,
@@ -447,11 +449,11 @@ begin
   exact_mod_cast (enat.add_one_le_of_lt hq)
 end
 
-lemma root_multiplicity_le_one_of_seperable {p : polynomial F} (hp : p ≠ 0)
+lemma root_multiplicity_le_one_of_separable {p : polynomial F} (hp : p ≠ 0)
   (hsep : separable p) (x : F) : root_multiplicity x p ≤ 1 :=
 begin
   rw [root_multiplicity_eq_multiplicity, dif_neg hp, ← enat.coe_le_coe, enat.coe_get],
-  exact multiplicity_le_one_of_seperable (not_unit_X_sub_C _) hsep
+  exact multiplicity_le_one_of_separable (not_unit_X_sub_C _) hsep
 end
 
 lemma count_roots_le_one {p : polynomial F} (hsep : separable p) (x : F) :
@@ -460,7 +462,7 @@ begin
   by_cases hp : p = 0,
   { simp [hp] },
   rw count_roots hp,
-  exact root_multiplicity_le_one_of_seperable hp hsep x
+  exact root_multiplicity_le_one_of_separable hp hsep x
 end
 
 lemma nodup_roots {p : polynomial F} (hsep : separable p) :
@@ -520,7 +522,8 @@ begin
   obtain ⟨hx, hs⟩ := h (algebra_map K E x),
   have hx' : is_integral F x := is_integral_tower_bot_of_is_integral_field hx,
   obtain ⟨q, hq⟩ := minimal_polynomial.dvd hx'
-    (is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero_field (minimal_polynomial.aeval hx)),
+    (is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero_field
+      (minimal_polynomial.aeval hx)),
   use hx',
   apply polynomial.separable.of_mul_left,
   rw ← hq,