refactor(*): rename is_group_hom.mul to map_mul (#911)

* refactor(*): rename is_group_hom.mul to map_mul

* Fix splits_mul

Author: jcommelin

src/algebra/big_operators.lean

@@ -615,38 +615,38 @@ section group
 open list
 variables [group α] [group β]
 
-@[to_additive is_add_group_hom.sum]
-theorem is_group_hom.prod (f : α → β) [is_group_hom f] (l : list α) :
+@[to_additive is_add_group_hom.map_sum]
+theorem is_group_hom.map_prod (f : α → β) [is_group_hom f] (l : list α) :
   f (prod l) = prod (map f l) :=
-by induction l; simp only [*, is_group_hom.mul f, is_group_hom.one f, prod_nil, prod_cons, map]
+by induction l; simp only [*, is_group_hom.map_mul f, is_group_hom.map_one f, prod_nil, prod_cons, map]
 
-theorem is_group_anti_hom.prod (f : α → β) [is_group_anti_hom f] (l : list α) :
+theorem is_group_anti_hom.map_prod (f : α → β) [is_group_anti_hom f] (l : list α) :
   f (prod l) = prod (map f (reverse l)) :=
-by induction l with hd tl ih; [exact is_group_anti_hom.one f,
-  simp only [prod_cons, is_group_anti_hom.mul f, ih, reverse_cons, map_append, prod_append, map_singleton, prod_cons, prod_nil, mul_one]]
+by induction l with hd tl ih; [exact is_group_anti_hom.map_one f,
+  simp only [prod_cons, is_group_anti_hom.map_mul f, ih, reverse_cons, map_append, prod_append, map_singleton, prod_cons, prod_nil, mul_one]]
 
 theorem inv_prod : ∀ l : list α, (prod l)⁻¹ = prod (map (λ x, x⁻¹) (reverse l)) :=
-λ l, @is_group_anti_hom.prod _ _ _ _ _ inv_is_group_anti_hom l -- TODO there is probably a cleaner proof of this
+λ l, @is_group_anti_hom.map_prod _ _ _ _ _ inv_is_group_anti_hom l -- TODO there is probably a cleaner proof of this
 
 end group
 
 section comm_group
 variables [comm_group α] [comm_group β] (f : α → β) [is_group_hom f]
 
 @[to_additive is_add_group_hom.multiset_sum]
-lemma is_group_hom.multiset_prod (m : multiset α) : f m.prod = (m.map f).prod :=
-quotient.induction_on m $ assume l, by simp [is_group_hom.prod f l]
+lemma is_group_hom.map_multiset_prod (m : multiset α) : f m.prod = (m.map f).prod :=
+quotient.induction_on m $ assume l, by simp [is_group_hom.map_prod f l]
 
 @[to_additive is_add_group_hom.finset_sum]
 lemma is_group_hom.finset_prod (g : γ → α) (s : finset γ) : f (s.prod g) = s.prod (f ∘ g) :=
-show f (s.val.map g).prod = (s.val.map (f ∘ g)).prod, by rw [is_group_hom.multiset_prod f]; simp
+show f (s.val.map g).prod = (s.val.map (f ∘ g)).prod, by rw [is_group_hom.map_multiset_prod f]; simp
 
 end comm_group
 
 @[to_additive is_add_group_hom_finset_sum]
 lemma is_group_hom_finset_prod {α β γ} [group α] [comm_group β] (s : finset γ)
   (f : γ → α → β) [∀c, is_group_hom (f c)] : is_group_hom (λa, s.prod (λc, f c a)) :=
-⟨assume a b, by simp only [λc, is_group_hom.mul (f c), finset.prod_mul_distrib]⟩
+⟨assume a b, by simp only [λc, is_group_hom.map_mul (f c), finset.prod_mul_distrib]⟩
 
 attribute [instance] is_group_hom_finset_prod is_add_group_hom_finset_sum
 

src/algebra/direct_sum.lean

@@ -33,31 +33,31 @@ instance mk.is_add_group_hom (s : finset ι) : is_add_group_hom (mk β s) :=
 ⟨λ _ _, dfinsupp.mk_add⟩
 
 @[simp] lemma mk_zero (s : finset ι) : mk β s 0 = 0 :=
-is_add_group_hom.zero _
+is_add_group_hom.map_zero _
 
 @[simp] lemma mk_add (s : finset ι) (x y) : mk β s (x + y) = mk β s x + mk β s y :=
-is_add_group_hom.add _ x y
+is_add_group_hom.map_add _ x y
 
 @[simp] lemma mk_neg (s : finset ι) (x) : mk β s (-x) = -mk β s x :=
-is_add_group_hom.neg _ x
+is_add_group_hom.map_neg _ x
 
 @[simp] lemma mk_sub (s : finset ι) (x y) : mk β s (x - y) = mk β s x - mk β s y :=
-is_add_group_hom.sub _ x y
+is_add_group_hom.map_sub _ x y
 
 instance of.is_add_group_hom (i : ι) : is_add_group_hom (of β i) :=
 ⟨λ _ _, dfinsupp.single_add⟩
 
 @[simp] lemma of_zero (i : ι) : of β i 0 = 0 :=
-is_add_group_hom.zero _
+is_add_group_hom.map_zero _
 
 @[simp] lemma of_add (i : ι) (x y) : of β i (x + y) = of β i x + of β i y :=
-is_add_group_hom.add _ x y
+is_add_group_hom.map_add _ x y
 
 @[simp] lemma of_neg (i : ι) (x) : of β i (-x) = -of β i x :=
-is_add_group_hom.neg _ x
+is_add_group_hom.map_neg _ x
 
 @[simp] lemma of_sub (i : ι) (x y) : of β i (x - y) = of β i x - of β i y :=
-is_add_group_hom.sub _ x y
+is_add_group_hom.map_sub _ x y
 
 theorem mk_inj (s : finset ι) : function.injective (mk β s) :=
 dfinsupp.mk_inj s
@@ -88,11 +88,11 @@ begin
   refine (finset.sum_subset H1 _).symm.trans ((finset.sum_congr rfl _).trans (finset.sum_subset H2 _)),
   { intros i H1 H2, rw finset.mem_inter at H2, rw H i,
     simp only [multiset.mem_to_finset] at H1 H2,
-    rw [(y.3 i).resolve_left (mt (and.intro H1) H2), is_add_group_hom.zero (φ i)] },
+    rw [(y.3 i).resolve_left (mt (and.intro H1) H2), is_add_group_hom.map_zero (φ i)] },
   { intros i H1, rw H i },
   { intros i H1 H2, rw finset.mem_inter at H2, rw ← H i,
     simp only [multiset.mem_to_finset] at H1 H2,
-    rw [(x.3 i).resolve_left (mt (λ H3, and.intro H3 H1) H2), is_add_group_hom.zero (φ i)] }
+    rw [(x.3 i).resolve_left (mt (λ H3, and.intro H3 H1) H2), is_add_group_hom.map_zero (φ i)] }
 end
 variables {φ}
 
@@ -102,31 +102,31 @@ begin
   refine quotient.induction_on f (λ x, _),
   refine quotient.induction_on g (λ y, _),
   change finset.sum _ _ = finset.sum _ _ + finset.sum _ _,
-  simp only, conv { to_lhs, congr, skip, funext, rw is_add_group_hom.add (φ i) },
+  simp only, conv { to_lhs, congr, skip, funext, rw is_add_group_hom.map_add (φ i) },
   simp only [finset.sum_add_distrib],
   congr' 1,
   { refine (finset.sum_subset _ _).symm,
     { intro i, simp only [multiset.mem_to_finset, multiset.mem_add], exact or.inl },
     { intros i H1 H2, simp only [multiset.mem_to_finset, multiset.mem_add] at H2,
-      rw [(x.3 i).resolve_left H2, is_add_group_hom.zero (φ i)] } },
+      rw [(x.3 i).resolve_left H2, is_add_group_hom.map_zero (φ i)] } },
   { refine (finset.sum_subset _ _).symm,
     { intro i, simp only [multiset.mem_to_finset, multiset.mem_add], exact or.inr },
     { intros i H1 H2, simp only [multiset.mem_to_finset, multiset.mem_add] at H2,
-      rw [(y.3 i).resolve_left H2, is_add_group_hom.zero (φ i)] } }
+      rw [(y.3 i).resolve_left H2, is_add_group_hom.map_zero (φ i)] } }
 end
 
 variables (φ)
 @[simp] lemma to_group_zero : to_group φ 0 = 0 :=
-is_add_group_hom.zero _
+is_add_group_hom.map_zero _
 
 @[simp] lemma to_group_add (x y) : to_group φ (x + y) = to_group φ x + to_group φ y :=
-is_add_group_hom.add _ x y
+is_add_group_hom.map_add _ x y
 
 @[simp] lemma to_group_neg (x) : to_group φ (-x) = -to_group φ x :=
-is_add_group_hom.neg _ x
+is_add_group_hom.map_neg _ x
 
 @[simp] lemma to_group_sub (x y) : to_group φ (x - y) = to_group φ x - to_group φ y :=
-is_add_group_hom.sub _ x y
+is_add_group_hom.map_sub _ x y
 
 @[simp] lemma to_group_of (i) (x : β i) : to_group φ (of β i x) = φ i x :=
 (add_zero _).trans $ congr_arg (φ i) $ show (if H : i ∈ finset.singleton i then x else 0) = x,
@@ -136,9 +136,9 @@ variables (ψ : direct_sum ι β → γ) [is_add_group_hom ψ]
 
 theorem to_group.unique (f : direct_sum ι β) : ψ f = to_group (λ i, ψ ∘ of β i) f :=
 direct_sum.induction_on f
-  (by rw [is_add_group_hom.zero ψ, is_add_group_hom.zero (to_group (λ i, ψ ∘ of β i))])
+  (by rw [is_add_group_hom.map_zero ψ, is_add_group_hom.map_zero (to_group (λ i, ψ ∘ of β i))])
   (λ i x, by rw [to_group_of])
-  (λ x y ihx ihy, by rw [is_add_group_hom.add ψ, is_add_group_hom.add (to_group (λ i, ψ ∘ of β i)), ihx, ihy])
+  (λ x y ihx ihy, by rw [is_add_group_hom.map_add ψ, is_add_group_hom.map_add (to_group (λ i, ψ ∘ of β i)), ihx, ihy])
 
 variables (β)
 def set_to_set (S T : set ι) (H : S ⊆ T) :

src/algebra/group.lean

@@ -664,14 +664,12 @@ by refine_struct {..}; simp [add_mul]
 
 end is_monoid_hom
 
--- TODO rename fields of is_group_hom: mul ↝ map_mul?
-
 /-- Predicate for group homomorphism. -/
 class is_group_hom [group α] [group β] (f : α → β) : Prop :=
-(mul : ∀ a b : α, f (a * b) = f a * f b)
+(map_mul : ∀ a b : α, f (a * b) = f a * f b)
 
 class is_add_group_hom [add_group α] [add_group β] (f : α → β) : Prop :=
-(add : ∀ a b, f (a + b) = f a + f b)
+(map_add : ∀ a b, f (a + b) = f a + f b)
 
 attribute [to_additive is_add_group_hom] is_group_hom
 attribute [to_additive is_add_group_hom.cases_on] is_group_hom.cases_on
@@ -680,29 +678,29 @@ attribute [to_additive is_add_group_hom.rec] is_group_hom.rec
 attribute [to_additive is_add_group_hom.drec] is_group_hom.drec
 attribute [to_additive is_add_group_hom.rec_on] is_group_hom.rec_on
 attribute [to_additive is_add_group_hom.drec_on] is_group_hom.drec_on
-attribute [to_additive is_add_group_hom.add] is_group_hom.mul
+attribute [to_additive is_add_group_hom.map_add] is_group_hom.map_mul
 attribute [to_additive is_add_group_hom.mk] is_group_hom.mk
 
 instance additive.is_add_group_hom [group α] [group β] (f : α → β) [is_group_hom f] :
   @is_add_group_hom (additive α) (additive β) _ _ f :=
-⟨@is_group_hom.mul α β _ _ f _⟩
+⟨@is_group_hom.map_mul α β _ _ f _⟩
 
 instance multiplicative.is_group_hom [add_group α] [add_group β] (f : α → β) [is_add_group_hom f] :
   @is_group_hom (multiplicative α) (multiplicative β) _ _ f :=
-⟨@is_add_group_hom.add α β _ _ f _⟩
+⟨@is_add_group_hom.map_add α β _ _ f _⟩
 
 attribute [to_additive additive.is_add_group_hom] multiplicative.is_group_hom
 
 namespace is_group_hom
 variables [group α] [group β] (f : α → β) [is_group_hom f]
 
-@[to_additive is_add_group_hom.zero]
-theorem one : f 1 = 1 :=
-mul_self_iff_eq_one.1 $ by rw [← mul f, one_mul]
+@[to_additive is_add_group_hom.map_zero]
+theorem map_one : f 1 = 1 :=
+mul_self_iff_eq_one.1 $ by rw [← map_mul f, one_mul]
 
-@[to_additive is_add_group_hom.neg]
-theorem inv (a : α) : f a⁻¹ = (f a)⁻¹ :=
-eq_inv_of_mul_eq_one $ by rw [← mul f, inv_mul_self, one f]
+@[to_additive is_add_group_hom.map_neg]
+theorem map_inv (a : α) : f a⁻¹ = (f a)⁻¹ :=
+eq_inv_of_mul_eq_one $ by rw [← map_mul f, inv_mul_self, map_one f]
 
 @[to_additive is_add_group_hom.id]
 instance id : is_group_hom (@id α) :=
@@ -711,42 +709,42 @@ instance id : is_group_hom (@id α) :=
 @[to_additive is_add_group_hom.comp]
 instance comp {γ} [group γ] (g : β → γ) [is_group_hom g] :
   is_group_hom (g ∘ f) :=
-⟨λ x y, show g _ = g _ * g _, by rw [mul f, mul g]⟩
+⟨λ x y, show g _ = g _ * g _, by rw [map_mul f, map_mul g]⟩
 
 protected lemma is_conj (f : α → β) [is_group_hom f] {a b : α} : is_conj a b → is_conj (f a) (f b)
-| ⟨c, hc⟩ := ⟨f c, by rw [← is_group_hom.mul f, ← is_group_hom.inv f, ← is_group_hom.mul f, hc]⟩
+| ⟨c, hc⟩ := ⟨f c, by rw [← is_group_hom.map_mul f, ← is_group_hom.map_inv f, ← is_group_hom.map_mul f, hc]⟩
 
 @[to_additive is_add_group_hom.to_is_add_monoid_hom]
 lemma to_is_monoid_hom (f : α → β) [is_group_hom f] : is_monoid_hom f :=
-⟨is_group_hom.one f, is_group_hom.mul f⟩
+⟨is_group_hom.map_one f, is_group_hom.map_mul f⟩
 
 @[to_additive is_add_group_hom.injective_iff]
 lemma injective_iff (f : α → β) [is_group_hom f] :
   function.injective f ↔ (∀ a, f a = 1 → a = 1) :=
-⟨λ h _, by rw ← is_group_hom.one f; exact @h _ _,
-  λ h x y hxy, by rw [← inv_inv (f x), inv_eq_iff_mul_eq_one, ← is_group_hom.inv f,
-      ← is_group_hom.mul f] at hxy;
+⟨λ h _, by rw ← is_group_hom.map_one f; exact @h _ _,
+  λ h x y hxy, by rw [← inv_inv (f x), inv_eq_iff_mul_eq_one, ← is_group_hom.map_inv f,
+      ← is_group_hom.map_mul f] at hxy;
     simpa using inv_eq_of_mul_eq_one (h _ hxy)⟩
 
 attribute [instance] is_group_hom.to_is_monoid_hom
   is_add_group_hom.to_is_add_monoid_hom
 
 end is_group_hom
 
-@[to_additive is_add_group_hom_add]
-lemma is_group_hom_mul {α β} [group α] [comm_group β]
+@[to_additive is_add_group_hom.add]
+lemma is_group_hom.mul {α β} [group α] [comm_group β]
   (f g : α → β) [is_group_hom f] [is_group_hom g] :
   is_group_hom (λa, f a * g a) :=
-⟨assume a b, by simp only [is_group_hom.mul f, is_group_hom.mul g, mul_comm, mul_assoc, mul_left_comm]⟩
+⟨assume a b, by simp only [is_group_hom.map_mul f, is_group_hom.map_mul g, mul_comm, mul_assoc, mul_left_comm]⟩
 
-attribute [instance] is_group_hom_mul is_add_group_hom_add
+attribute [instance] is_group_hom.mul is_add_group_hom.add
 
-@[to_additive is_add_group_hom_neg]
-lemma is_group_hom_inv {α β} [group α] [comm_group β] (f : α → β) [is_group_hom f] :
+@[to_additive is_add_group_hom.neg]
+lemma is_group_hom.inv {α β} [group α] [comm_group β] (f : α → β) [is_group_hom f] :
   is_group_hom (λa, (f a)⁻¹) :=
-⟨assume a b, by rw [is_group_hom.mul f, mul_inv]⟩
+⟨assume a b, by rw [is_group_hom.map_mul f, mul_inv]⟩
 
-attribute [instance] is_group_hom_inv is_add_group_hom_neg
+attribute [instance] is_group_hom.inv is_add_group_hom.neg
 
 @[to_additive neg.is_add_group_hom]
 lemma inv.is_group_hom [comm_group α] : is_group_hom (has_inv.inv : α → α) :=
@@ -757,17 +755,17 @@ attribute [instance] inv.is_group_hom neg.is_add_group_hom
 /-- Predicate for group anti-homomorphism, or a homomorphism
   into the opposite group. -/
 class is_group_anti_hom {β : Type*} [group α] [group β] (f : α → β) : Prop :=
-(mul : ∀ a b : α, f (a * b) = f b * f a)
+(map_mul : ∀ a b : α, f (a * b) = f b * f a)
 
 namespace is_group_anti_hom
 variables [group α] [group β] (f : α → β) [w : is_group_anti_hom f]
 include w
 
-theorem one : f 1 = 1 :=
-mul_self_iff_eq_one.1 $ by rw [← mul f, one_mul]
+theorem map_one : f 1 = 1 :=
+mul_self_iff_eq_one.1 $ by rw [← map_mul f, one_mul]
 
-theorem inv (a : α) : f a⁻¹ = (f a)⁻¹ :=
-eq_inv_of_mul_eq_one $ by rw [← mul f, mul_inv_self, one f]
+theorem map_inv (a : α) : f a⁻¹ = (f a)⁻¹ :=
+eq_inv_of_mul_eq_one $ by rw [← map_mul f, mul_inv_self, map_one f]
 
 end is_group_anti_hom
 
@@ -777,19 +775,19 @@ theorem inv_is_group_anti_hom [group α] : is_group_anti_hom (λ x : α, x⁻¹)
 namespace is_add_group_hom
 variables [add_group α] [add_group β] (f : α → β) [is_add_group_hom f]
 
-lemma sub (a b) : f (a - b) = f a - f b :=
+lemma map_sub (a b) : f (a - b) = f a - f b :=
 calc f (a - b) = f (a + -b)   : rfl
-           ... = f a + f (-b) : add f _ _
-           ... = f a - f b    : by  simp[neg f]
+           ... = f a + f (-b) : map_add f _ _
+           ... = f a - f b    : by  simp[map_neg f]
 
 end is_add_group_hom
 
-lemma is_add_group_hom_sub {α β} [add_group α] [add_comm_group β]
+lemma is_add_group_hom.sub {α β} [add_group α] [add_comm_group β]
   (f g : α → β) [is_add_group_hom f] [is_add_group_hom g] :
   is_add_group_hom (λa, f a - g a) :=
-is_add_group_hom_add f (λa, - g a)
+is_add_group_hom.add f (λa, - g a)
 
-attribute [instance] is_add_group_hom_sub
+attribute [instance] is_add_group_hom.sub
 
 namespace units
 

src/algebra/group_power.lean

@@ -354,27 +354,27 @@ end group
 namespace is_group_hom
 variables {β : Type v} [group α] [group β] (f : α → β) [is_group_hom f]
 
-theorem pow (a : α) (n : ℕ) : f (a ^ n) = f a ^ n :=
+theorem map_pow (a : α) (n : ℕ) : f (a ^ n) = f a ^ n :=
 is_monoid_hom.map_pow f a n
 
-theorem gpow (a : α) (n : ℤ) : f (a ^ n) = f a ^ n :=
-by cases n; [exact is_group_hom.pow f _ _,
-  exact (is_group_hom.inv f _).trans (congr_arg _ $ is_group_hom.pow f _ _)]
+theorem map_gpow (a : α) (n : ℤ) : f (a ^ n) = f a ^ n :=
+by cases n; [exact is_group_hom.map_pow f _ _,
+  exact (is_group_hom.map_inv f _).trans (congr_arg _ $ is_group_hom.map_pow f _ _)]
 
 end is_group_hom
 
 namespace is_add_group_hom
 variables {β : Type v} [add_group α] [add_group β] (f : α → β) [is_add_group_hom f]
 
-theorem smul (a : α) (n : ℕ) : f (n • a) = n • f a :=
+theorem map_smul (a : α) (n : ℕ) : f (n • a) = n • f a :=
 is_add_monoid_hom.map_smul f a n
 
-theorem gsmul (a : α) (n : ℤ) : f (gsmul n a) = gsmul n (f a) :=
+theorem map_gsmul (a : α) (n : ℤ) : f (gsmul n a) = gsmul n (f a) :=
 begin
   induction n using int.induction_on with z ih z ih,
-  { simp [is_add_group_hom.zero f] },
-  { simp [is_add_group_hom.add f, add_gsmul, ih] },
-  { simp [is_add_group_hom.add f, is_add_group_hom.neg f, add_gsmul, ih] }
+  { simp [is_add_group_hom.map_zero f] },
+  { simp [is_add_group_hom.map_add f, add_gsmul, ih] },
+  { simp [is_add_group_hom.map_add f, is_add_group_hom.map_neg f, add_gsmul, ih] }
 end
 
 end is_add_group_hom
@@ -407,10 +407,10 @@ end comm_monoid
 section group
 
 @[instance]
-theorem is_add_group_hom_gsmul
+theorem is_add_group_hom.gsmul
   {α β} [add_group α] [add_comm_group β] (f : α → β) [is_add_group_hom f] (z : ℤ) :
   is_add_group_hom (λa, gsmul z (f a)) :=
-⟨assume a b, by rw [is_add_group_hom.add f, gsmul_add]⟩
+⟨assume a b, by rw [is_add_group_hom.map_add f, gsmul_add]⟩
 
 end group
 

src/analysis/complex/exponential.lean

@@ -484,7 +484,7 @@ instance angle.is_add_group_hom : is_add_group_hom (coe : ℝ → angle) :=
 @[simp] lemma coe_add (x y : ℝ) : ↑(x + y : ℝ) = (↑x + ↑y : angle) := rfl
 @[simp] lemma coe_neg (x : ℝ) : ↑(-x : ℝ) = -(↑x : angle) := rfl
 @[simp] lemma coe_sub (x y : ℝ) : ↑(x - y : ℝ) = (↑x - ↑y : angle) := rfl
-@[simp] lemma coe_gsmul (x : ℝ) (n : ℤ) : ↑(gsmul n x : ℝ) = gsmul n (↑x : angle) := is_add_group_hom.gsmul _ _ _
+@[simp] lemma coe_gsmul (x : ℝ) (n : ℤ) : ↑(gsmul n x : ℝ) = gsmul n (↑x : angle) := is_add_group_hom.map_gsmul _ _ _
 @[simp] lemma coe_two_pi : ↑(2 * π : ℝ) = (0 : angle) :=
 quotient.sound' ⟨-1, by dsimp only; rw [neg_one_gsmul, add_zero]⟩
 

src/field_theory/splitting_field.lean

@@ -62,7 +62,7 @@ end
 lemma splits_mul {f g : polynomial α} (hf : splits i f) (hg : splits i g) : splits i (f * g) :=
 if h : f * g = 0 then by simp [h]
 else or.inr $ λ p hp hpf, ((principal_ideal_domain.irreducible_iff_prime.1 hp).2.2 _ _
-    (show p ∣ map i f * map i g, by convert hpf; rw map_mul)).elim
+    (show p ∣ map i f * map i g, by convert hpf; rw polynomial.map_mul)).elim
   (hf.resolve_left (λ hf, by simpa [hf] using h) hp)
   (hg.resolve_left (λ hg, by simpa [hg] using h) hp)