chore(data/polynomial/monic): dedup degree_map (#11792)

Author: ericrbg

src/data/polynomial/monic.lean

@@ -318,34 +318,30 @@ else degree_map_eq_of_leading_coeff_ne_zero _
   (by rw [← f.map_zero]; exact mt hf.eq_iff.1
     (mt leading_coeff_eq_zero.1 h))
 
-lemma degree_map' (p : polynomial R) :
-  degree (p.map f) = degree p :=
-p.degree_map_eq_of_injective hf
-
-lemma nat_degree_map' (p : polynomial R) :
+lemma nat_degree_map_eq_of_injective (p : polynomial R) :
   nat_degree (p.map f) = nat_degree p :=
-nat_degree_eq_of_degree_eq (degree_map' hf p)
+nat_degree_eq_of_degree_eq (degree_map_eq_of_injective hf p)
 
 lemma leading_coeff_map' (p : polynomial R) :
   leading_coeff (p.map f) = f (leading_coeff p) :=
 begin
   unfold leading_coeff,
-  rw [coeff_map, nat_degree_map' hf p],
+  rw [coeff_map, nat_degree_map_eq_of_injective hf p],
 end
 
 lemma next_coeff_map (p : polynomial R) :
   (p.map f).next_coeff = f p.next_coeff :=
 begin
   unfold next_coeff,
-  rw nat_degree_map' hf,
+  rw nat_degree_map_eq_of_injective hf,
   split_ifs; simp
 end
 
 lemma leading_coeff_of_injective (p : polynomial R) :
   leading_coeff (p.map f) = f (leading_coeff p) :=
 begin
   delta leading_coeff,
-  rw [coeff_map f, nat_degree_map' hf p]
+  rw [coeff_map f, nat_degree_map_eq_of_injective hf p]
 end
 
 lemma monic_of_injective {p : polynomial R} (hp : (p.map f).monic) : p.monic :=

src/field_theory/splitting_field.lean

@@ -419,7 +419,7 @@ begin
     congr' 1,
     rw ← this,
     simp, },
-  { rw [nat_degree_map' (is_fraction_ring.injective K (fraction_ring K)), ← this],
+  { rw [nat_degree_map_eq_of_injective (is_fraction_ring.injective K (fraction_ring K)), ← this],
     simp only [←hroots, multiset.card_map], },
 end
 
@@ -466,7 +466,7 @@ begin
       (is_fraction_ring.injective K (fraction_ring K)) hroots,
   have : multiset.card (map (algebra_map K (fraction_ring K)) p).roots =
     (map (algebra_map K (fraction_ring K)) p).nat_degree,
-  { rw [nat_degree_map' (is_fraction_ring.injective K (fraction_ring K)), ← h],
+  { rw [nat_degree_map_eq_of_injective (is_fraction_ring.injective K (fraction_ring K)), ← h],
     simp only [←hroots, multiset.card_map], },
   rw [← C_leading_coeff_mul_prod_multiset_X_sub_C_of_field this],
   simp only [map_C, function.comp_app, map_X, map_sub],

src/ring_theory/algebraic.lean

@@ -140,7 +140,7 @@ lemma _root_.is_algebraic_of_larger_base_of_injective (hinj : function.injective
   {x : A} (A_alg : _root_.is_algebraic R x) : _root_.is_algebraic S x :=
 let ⟨p, hp₁, hp₂⟩ := A_alg in
 ⟨p.map (algebra_map _ _),
-  by rwa [ne.def, ← degree_eq_bot, degree_map' hinj, degree_eq_bot],
+  by rwa [ne.def, ← degree_eq_bot, degree_map_eq_of_injective hinj, degree_eq_bot],
   by simpa⟩
 
 /-- If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R,

src/ring_theory/polynomial/gauss_lemma.lean

@@ -42,7 +42,7 @@ begin
   refine ⟨(map_ring_hom φ).is_unit_map, λ h, _⟩,
   rcases is_unit_iff.1 h with ⟨_, ⟨u, rfl⟩, hu⟩,
   have hdeg := degree_C u.ne_zero,
-  rw [hu, degree_map' hinj] at hdeg,
+  rw [hu, degree_map_eq_of_injective hinj] at hdeg,
   rw [eq_C_of_degree_eq_zero hdeg, is_primitive_iff_content_eq_one,
       content_C, normalize_eq_one] at hf,
   rwa [eq_C_of_degree_eq_zero hdeg, is_unit_C],