[Merged by Bors] - feat(data/polynomial/eval): add protected on some lemmas about polynomial.map

src/algebra/polynomial/group_ring_action.lean

@@ -40,8 +40,10 @@ variables (M)
 
 noncomputable instance [mul_semiring_action M R] : mul_semiring_action M R[X] :=
 { smul := (•),
-  smul_one := λ m, (smul_eq_map R m).symm ▸ map_one (mul_semiring_action.to_ring_hom M R m),
-  smul_mul := λ m p q, (smul_eq_map R m).symm ▸ map_mul (mul_semiring_action.to_ring_hom M R m),
+  smul_one := λ m,
+    (smul_eq_map R m).symm ▸ polynomial.map_one (mul_semiring_action.to_ring_hom M R m),
+  smul_mul := λ m p q,
+    (smul_eq_map R m).symm ▸ polynomial.map_mul (mul_semiring_action.to_ring_hom M R m),
   ..polynomial.distrib_mul_action }
 
 variables {M R}

src/data/polynomial/derivative.lean

@@ -261,13 +261,14 @@ end
 theorem derivative_map [comm_semiring S] (p : R[X]) (f : R →+* S) :
   (p.map f).derivative = p.derivative.map f :=
 polynomial.induction_on p
-  (λ r, by rw [map_C, derivative_C, derivative_C, map_zero])
-  (λ p q ihp ihq, by rw [map_add, derivative_add, ihp, ihq, derivative_add, map_add])
-  (λ n r ih, by rw [map_mul, map_C, polynomial.map_pow, map_X, derivative_mul, derivative_pow_succ,
-                    derivative_C, zero_mul, zero_add, derivative_X, mul_one, derivative_mul,
-                    derivative_pow_succ, derivative_C, zero_mul, zero_add, derivative_X, mul_one,
-                    map_mul, map_C, map_mul, polynomial.map_pow, map_add,
-                    polynomial.map_nat_cast, map_one, map_X])
+  (λ r, by rw [map_C, derivative_C, derivative_C, polynomial.map_zero])
+  (λ p q ihp ihq, by rw [polynomial.map_add, derivative_add, ihp, ihq, derivative_add,
+                         polynomial.map_add])
+  (λ n r ih, by rw [polynomial.map_mul, polynomial.map_C, polynomial.map_pow, polynomial.map_X,
+    derivative_mul, derivative_pow_succ, derivative_C, zero_mul, zero_add, derivative_X, mul_one,
+    derivative_mul, derivative_pow_succ, derivative_C, zero_mul, zero_add, derivative_X, mul_one,
+    polynomial.map_mul, polynomial.map_C, polynomial.map_mul, polynomial.map_pow,
+    polynomial.map_add, polynomial.map_nat_cast, polynomial.map_one, polynomial.map_X])
 
 @[simp]
 theorem iterate_derivative_map [comm_semiring S] (p : R[X]) (f : R →+* S) (k : ℕ):

src/data/polynomial/div.lean

@@ -301,7 +301,7 @@ begin
   haveI : nontrivial R := f.domain_nontrivial,
   have : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q),
   { exact (div_mod_by_monic_unique ((p /ₘ q).map f) _ (hq.map f)
-      ⟨eq.symm $ by rw [← map_mul, ← map_add, mod_by_monic_add_div _ hq],
+      ⟨eq.symm $ by rw [← polynomial.map_mul, ← polynomial.map_add, mod_by_monic_add_div _ hq],
       calc _ ≤ degree (p %ₘ q) : degree_map_le _ _
       ... < degree q : degree_mod_by_monic_lt _ hq
       ... = _ : eq.symm $ degree_map_eq_of_leading_coeff_ne_zero _
@@ -343,8 +343,8 @@ theorem map_dvd_map [comm_ring S] (f : R →+* S) (hf : function.injective f) {x
 begin
   rw [← dvd_iff_mod_by_monic_eq_zero hx, ← dvd_iff_mod_by_monic_eq_zero (hx.map f),
     ← map_mod_by_monic f hx],
-  exact ⟨λ H, map_injective f hf $ by rw [H, map_zero],
-  λ H, by rw [H, map_zero]⟩
+  exact ⟨λ H, map_injective f hf $ by rw [H, polynomial.map_zero],
+  λ H, by rw [H, polynomial.map_zero]⟩
 end
 
 @[simp] lemma mod_by_monic_one (p : R[X]) : p %ₘ 1 = 0 :=

src/data/polynomial/eval.lean

@@ -510,13 +510,13 @@ begin
   rw [eval₂_monomial, monomial_eq_C_mul_X], refl,
 end
 
-@[simp] lemma map_zero : (0 : R[X]).map f = 0 :=  eval₂_zero _ _
+@[simp] protected lemma map_zero : (0 : R[X]).map f = 0 :=  eval₂_zero _ _
 
-@[simp] lemma map_add : (p + q).map f = p.map f + q.map f := eval₂_add _ _
+@[simp] protected lemma map_add : (p + q).map f = p.map f + q.map f := eval₂_add _ _
 
-@[simp] lemma map_one : (1 : R[X]).map f = 1 := eval₂_one _ _
+@[simp] protected lemma map_one : (1 : R[X]).map f = 1 := eval₂_one _ _
 
-@[simp] lemma map_mul : (p * q).map f = p.map f * q.map f :=
+@[simp] protected lemma map_mul : (p * q).map f = p.map f * q.map f :=
 by { rw [map, eval₂_mul_noncomm], exact λ k, (commute_X _).symm }
 
 @[simp] lemma map_smul (r : R) : (r • p).map f = f r • p.map f :=
@@ -531,10 +531,10 @@ by rw [map, eval₂_smul, ring_hom.comp_apply, C_mul']
 -- lean/blob/487ac5d7e9b34800502e1ddf3c7c806c01cf9d51/src/frontends/lean/elaborator.cpp#L1876-L1913
 def map_ring_hom (f : R →+* S) : R[X] →+* S[X] :=
 { to_fun := polynomial.map f,
-  map_add' := λ _ _, map_add f,
-  map_zero' := map_zero f,
-  map_mul' := λ _ _, map_mul f,
-  map_one' := map_one f }
+  map_add' := λ _ _, polynomial.map_add f,
+  map_zero' := polynomial.map_zero f,
+  map_mul' := λ _ _, polynomial.map_mul f,
+  map_one' := polynomial.map_one f }
 
 @[simp] lemma coe_map_ring_hom (f : R →+* S) : ⇑(map_ring_hom f) = map f := rfl
 
@@ -578,7 +578,8 @@ lemma map_injective (hf : function.injective f) : function.injective (map f) :=
 
 lemma map_surjective (hf : function.surjective f) : function.surjective (map f) :=
 λ p, polynomial.induction_on' p
- (λ p q hp hq, let ⟨p', hp'⟩ := hp, ⟨q', hq'⟩ := hq in ⟨p' + q', by rw [map_add f, hp', hq']⟩)
+ (λ p q hp hq, let ⟨p', hp'⟩ := hp, ⟨q', hq'⟩ := hq
+                 in ⟨p' + q', by rw [polynomial.map_add f, hp', hq']⟩)
  (λ n s, let ⟨r, hr⟩ := hf s in ⟨monomial n r, by rw [map_monomial f, hr]⟩)
 
 lemma degree_map_le (p : R[X]) : degree (p.map f) ≤ degree p :=
@@ -648,7 +649,7 @@ begin
     intros i hi,
     rcases h i with ⟨c, hc⟩,
     use [C c * X^i],
-    rw [coe_map_ring_hom, map_mul, map_C, hc, polynomial.map_pow, map_X] }
+    rw [coe_map_ring_hom, polynomial.map_mul, map_C, hc, polynomial.map_pow, map_X] }
 end
 
 lemma mem_map_range {R S : Type*} [ring R] [ring S] (f : R →+* S)
@@ -669,10 +670,10 @@ protected lemma map_sum {ι : Type*} (g : ι → R[X]) (s : finset ι) :
 lemma map_comp (p q : R[X]) : map f (p.comp q) = (map f p).comp (map f q) :=
 polynomial.induction_on p
   (by simp only [map_C, forall_const, C_comp, eq_self_iff_true])
-  (by simp only [map_add, add_comp, forall_const, implies_true_iff, eq_self_iff_true]
+  (by simp only [polynomial.map_add, add_comp, forall_const, implies_true_iff, eq_self_iff_true]
         {contextual := tt})
   (by simp only [pow_succ', ←mul_assoc, comp, forall_const, eval₂_mul_X, implies_true_iff,
-        eq_self_iff_true, map_X, map_mul] {contextual := tt})
+        eq_self_iff_true, map_X, polynomial.map_mul] {contextual := tt})
 
 @[simp]
 lemma eval_zero_map (f : R →+* S) (p : R[X]) :
@@ -684,7 +685,7 @@ lemma eval_one_map (f : R →+* S) (p : R[X]) :
   (p.map f).eval 1 = f (p.eval 1) :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
+  { intros p q hp hq, simp only [hp, hq, polynomial.map_add, ring_hom.map_add, eval_add] },
   { intros n r, simp only [one_pow, mul_one, eval_monomial, map_monomial] }
 end
 
@@ -693,7 +694,7 @@ lemma eval_nat_cast_map (f : R →+* S) (p : R[X]) (n : ℕ) :
   (p.map f).eval n = f (p.eval n) :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
+  { intros p q hp hq, simp only [hp, hq, polynomial.map_add, ring_hom.map_add, eval_add] },
   { intros n r, simp only [map_nat_cast f, eval_monomial, map_monomial, f.map_pow, f.map_mul] }
 end
 
@@ -703,7 +704,7 @@ lemma eval_int_cast_map {R S : Type*} [ring R] [ring S]
   (p.map f).eval i = f (p.eval i) :=
 begin
   apply polynomial.induction_on' p,
-  { intros p q hp hq, simp only [hp, hq, map_add, ring_hom.map_add, eval_add] },
+  { intros p q hp hq, simp only [hp, hq, polynomial.map_add, ring_hom.map_add, eval_add] },
   { intros n r, simp only [f.map_int_cast, eval_monomial, map_monomial, f.map_pow, f.map_mul] }
 end
 
@@ -877,11 +878,11 @@ lemma C_neg : C (-a) = -C a := ring_hom.map_neg C a
 
 lemma C_sub : C (a - b) = C a - C b := ring_hom.map_sub C a b
 
-@[simp] lemma map_sub {S} [ring S] (f : R →+* S) :
+@[simp] protected lemma map_sub {S} [ring S] (f : R →+* S) :
   (p - q).map f = p.map f - q.map f :=
 (map_ring_hom f).map_sub p q
 
-@[simp] lemma map_neg {S} [ring S] (f : R →+* S) :
+@[simp] protected lemma map_neg {S} [ring S] (f : R →+* S) :
   (-p).map f = -(p.map f) :=
 (map_ring_hom f).map_neg p
 

src/data/polynomial/field_division.lean

@@ -299,20 +299,21 @@ lemma map_div [field k] (f : R →+* k) :
   (p / q).map f = p.map f / q.map f :=
 if hq0 : q = 0 then by simp [hq0]
 else
-by rw [div_def, div_def, map_mul, map_div_by_monic f (monic_mul_leading_coeff_inv hq0)];
+by rw [div_def, div_def, polynomial.map_mul, map_div_by_monic f (monic_mul_leading_coeff_inv hq0)];
   simp [f.map_inv, coeff_map f]
 
 lemma map_mod [field k] (f : R →+* k) :
   (p % q).map f = p.map f % q.map f :=
 if hq0 : q = 0 then by simp [hq0]
 else by rw [mod_def, mod_def, leading_coeff_map f, ← f.map_inv, ← map_C f,
-  ← map_mul f, map_mod_by_monic f (monic_mul_leading_coeff_inv hq0)]
+  ← polynomial.map_mul f, map_mod_by_monic f (monic_mul_leading_coeff_inv hq0)]
 
 section
 open euclidean_domain
 theorem gcd_map [field k] (f : R →+* k) :
   gcd (p.map f) (q.map f) = (gcd p q).map f :=
-gcd.induction p q (λ x, by simp_rw [map_zero, euclidean_domain.gcd_zero_left]) $ λ x y hx ih,
+gcd.induction p q (λ x, by simp_rw [polynomial.map_zero, euclidean_domain.gcd_zero_left]) $
+                    λ x y hx ih,
 by rw [gcd_val, ← map_mod, ih, ← gcd_val]
 end
 
@@ -442,11 +443,11 @@ by simp [comm_group_with_zero.coe_norm_unit _ this]
 lemma normalize_monic (h : monic p) : normalize p = p := by simp [h]
 
 theorem map_dvd_map' [field k] (f : R →+* k) {x y : R[X]} : x.map f ∣ y.map f ↔ x ∣ y :=
-if H : x = 0 then by rw [H, map_zero, zero_dvd_iff, zero_dvd_iff, map_eq_zero]
+if H : x = 0 then by rw [H, polynomial.map_zero, zero_dvd_iff, zero_dvd_iff, map_eq_zero]
 else by rw [← normalize_dvd_iff, ← @normalize_dvd_iff R[X],
     normalize_apply, normalize_apply,
     coe_norm_unit_of_ne_zero H, coe_norm_unit_of_ne_zero (mt (map_eq_zero f).1 H),
-    leading_coeff_map, ← f.map_inv, ← map_C, ← map_mul,
+    leading_coeff_map, ← f.map_inv, ← map_C, ← polynomial.map_mul,
     map_dvd_map _ f.injective (monic_mul_leading_coeff_inv H)]
 
 lemma degree_normalize : degree (normalize p) = degree p := by simp

src/data/polynomial/lifts.lean

@@ -125,7 +125,8 @@ lemma monomial_mem_lifts_and_degree_eq {s : S} {n : ℕ} (hl : monomial n s ∈
 begin
   by_cases hzero : s = 0,
   { use 0,
-    simp only [hzero, degree_zero, eq_self_iff_true, and_self, monomial_zero_right, map_zero] },
+    simp only [hzero, degree_zero, eq_self_iff_true, and_self, monomial_zero_right,
+               polynomial.map_zero] },
   rw lifts_iff_set_range at hl,
   obtain ⟨q, hq⟩ := hl,
   replace hq := (ext_iff.1 hq) n,
@@ -172,7 +173,7 @@ begin
     (erase_mem_lifts p.nat_degree hlifts) (refl p.erase_lead.nat_degree),
   use erase + lead,
   split,
-  { simp only [hlead, herase, map_add],
+  { simp only [hlead, herase, polynomial.map_add],
     nth_rewrite 0 erase_lead_add_monomial_nat_degree_leading_coeff p },
   rw [←hdeg, erase_lead] at deg_erase,
   replace deg_erase := lt_of_le_of_lt degree_le_nat_degree (with_bot.coe_lt_coe.2 deg_erase),
@@ -204,7 +205,7 @@ begin
   { rw [@degree_X_pow R, hq.2, degree_eq_nat_degree h0, with_bot.coe_lt_coe],
     exact or.resolve_right (erase_lead_nat_degree_lt_or_erase_lead_eq_zero p) h0, },
   refine ⟨q + X ^ p.nat_degree, _, _, (monic_X_pow _).add_of_right hdeg⟩,
-  { rw [map_add, hq.1, polynomial.map_pow, map_X, H], },
+  { rw [polynomial.map_add, hq.1, polynomial.map_pow, map_X, H], },
   { rw [degree_add_eq_right_of_degree_lt hdeg, degree_X_pow, degree_eq_nat_degree hp.ne_zero] }
 end
 

src/data/polynomial/ring_division.lean

@@ -475,8 +475,8 @@ lemma le_root_multiplicity_map {K L : Type*} [comm_ring K]
   [comm_ring L] {p : K[X]} {f : K →+* L} (hf : function.injective f) (a : K) :
   root_multiplicity a p ≤ root_multiplicity (f a) (map f p) :=
 begin
-  by_cases hp0 : p = 0, { simp only [hp0, root_multiplicity_zero, map_zero], },
-  have hmap : map f p ≠ 0, { simpa only [map_zero] using (map_injective f hf).ne hp0, },
+  by_cases hp0 : p = 0, { simp only [hp0, root_multiplicity_zero, polynomial.map_zero], },
+  have hmap : map f p ≠ 0, { simpa only [polynomial.map_zero] using (map_injective f hf).ne hp0, },
   rw [root_multiplicity, root_multiplicity, dif_neg hp0, dif_neg hmap],
   simp only [not_not, nat.lt_find_iff, nat.le_find_iff],
   intros m hm,
@@ -505,8 +505,8 @@ lemma roots_map_of_injective_card_eq_total_degree {K L : Type*} [comm_ring K] [i
   (hroots : p.roots.card = p.nat_degree) :
   multiset.map f p.roots = (map f p).roots :=
 begin
-  by_cases hp0 : p = 0, { simp only [hp0, roots_zero, multiset.map_zero, map_zero], },
-  have hmap : map f p ≠ 0, { simpa only [map_zero] using (map_injective f hf).ne hp0, },
+  by_cases hp0 : p = 0, { simp only [hp0, roots_zero, multiset.map_zero, polynomial.map_zero], },
+  have hmap : map f p ≠ 0, { simpa only [polynomial.map_zero] using (map_injective f hf).ne hp0, },
   apply multiset.eq_of_le_of_card_le,
   { simpa only [multiset.le_iff_count, count_roots] using count_map_roots hf },
   { simpa only [multiset.card_map, hroots] using (card_roots' _).trans (nat_degree_map_le f p) },
@@ -638,7 +638,7 @@ begin
   rw [mem_root_set_iff', ←eval₂_eq_eval_map],
   { refl },
   intro h,
-  rw ←map_zero (algebra_map T S) at h,
+  rw ←polynomial.map_zero (algebra_map T S) at h,
   exact hp (map_injective _ (no_zero_smul_divisors.algebra_map_injective T S) h)
 end
 
@@ -773,7 +773,7 @@ begin
     clear q h_mon,
 
     have h' := congr_arg (map φ) h,
-    simp only [map_mul] at h',
+    simp only [polynomial.map_mul] at h',
     cases h_irr.is_unit_or_is_unit h' with w w,
     { left,
       exact is_unit_of_is_unit_leading_coeff_of_is_unit_map _ _ au w, },

src/field_theory/polynomial_galois_group.lean

@@ -238,7 +238,7 @@ begin
   dsimp only [restrict_prod, restrict_dvd] at hfg,
   simp only [dif_neg hpq, monoid_hom.prod_apply, prod.mk.inj_iff] at hfg,
   ext x hx,
-  rw [root_set, map_mul, polynomial.roots_mul] at hx,
+  rw [root_set, polynomial.map_mul, polynomial.roots_mul] at hx,
   cases multiset.mem_add.mp (multiset.mem_to_finset.mp hx) with h h,
   { haveI : fact (p.splits (algebra_map F (p * q).splitting_field)) :=
       ⟨splits_of_splits_of_dvd _ hpq (splitting_field.splits (p * q)) (dvd_mul_right p q)⟩,

src/field_theory/separable.lean

@@ -108,7 +108,8 @@ theorem separable.of_pow {f : R[X]} (hf : ¬is_unit f) {n : ℕ} (hn : n ≠ 0)
 
 theorem separable.map {p : R[X]} (h : p.separable) {f : R →+* S} : (p.map f).separable :=
 let ⟨a, b, H⟩ := h in ⟨a.map f, b.map f,
-by rw [derivative_map, ← map_mul, ← map_mul, ← map_add, H, map_one]⟩
+by rw [derivative_map, ← polynomial.map_mul, ← polynomial.map_mul, ← polynomial.map_add, H,
+       polynomial.map_one]⟩
 
 variables (R) (p q : ℕ)
 
@@ -307,7 +308,7 @@ include hp
 theorem expand_char (f : R[X]) : map (frobenius R p) (expand R p f) = f ^ p :=
 begin
   refine f.induction_on' (λ a b ha hb, _) (λ n a, _),
-  { rw [alg_hom.map_add, map_add, ha, hb, add_pow_char], },
+  { rw [alg_hom.map_add, polynomial.map_add, ha, hb, add_pow_char], },
   { rw [expand_monomial, map_monomial, monomial_eq_C_mul_X, monomial_eq_C_mul_X,
         mul_pow, ← C.map_pow, frobenius_def],
     ring_exp }