[Merged by Bors] - chore(field_theory/separable): generalize theorems

src/data/polynomial/algebra_map.lean

@@ -376,7 +376,7 @@ begin
   simp [sum_range_sub', coeff_monomial],
 end
 
-theorem not_is_unit_X_sub_C [nontrivial R] {r : R} : ¬ is_unit (X - C r) :=
+theorem not_is_unit_X_sub_C [nontrivial R] (r : R) : ¬ is_unit (X - C r) :=
 λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ $ by erw [← eval_mul_X_sub_C, hgf, eval_one]
 
 end ring

src/data/polynomial/ring_division.lean

@@ -171,7 +171,7 @@ by rw [nat_degree_one, nat_degree_mul hp0 hq0, eq_comm,
 degree_eq_zero_of_is_unit ⟨u, rfl⟩
 
 theorem prime_X_sub_C (r : R) : prime (X - C r) :=
-⟨X_sub_C_ne_zero r, not_is_unit_X_sub_C,
+⟨X_sub_C_ne_zero r, not_is_unit_X_sub_C r,
  λ _ _, by { simp_rw [dvd_iff_is_root, is_root.def, eval_mul, mul_eq_zero], exact id }⟩
 
 theorem prime_X : prime (X : polynomial R) :=

src/field_theory/finite/basic.lean

@@ -304,11 +304,12 @@ open polynomial
 lemma expand_card (f : polynomial K) :
   expand K q f = f ^ q :=
 begin
-  cases char_p.exists K with p hp, letI := hp,
-  rcases finite_field.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩, haveI : fact p.prime := ⟨hp⟩,
-  dsimp at hn, rw hn at *,
-  rw ← map_expand_pow_char,
-  rw [frobenius_pow hn, ring_hom.one_def, map_id],
+  cases char_p.exists K with p hp,
+  letI := hp,
+  rcases finite_field.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩,
+  haveI : fact p.prime := ⟨hp⟩,
+  dsimp at hn,
+  rw [hn, ← map_expand_pow_char, frobenius_pow hn, ring_hom.one_def, map_id]
 end
 
 end finite_field

src/field_theory/primitive_element.lean

@@ -154,7 +154,7 @@ begin
     apply (div_eq_iff (sub_ne_zero.mpr a)).mpr,
     simp only [algebra.smul_def, ring_hom.map_add, ring_hom.map_mul, ring_hom.comp_apply],
     ring },
-  rw ← eq_X_sub_C_of_separable_of_root_eq h_ne_zero h_sep h_root h_splits h_roots,
+  rw ← eq_X_sub_C_of_separable_of_root_eq h_sep h_root h_splits h_roots,
   transitivity euclidean_domain.gcd (_ : polynomial E) (_ : polynomial E),
   { dsimp only [p],
     convert (gcd_map (algebra_map F⟮γ⟯ E)).symm },