chore(Algebra/Group/TypeTags): Remove porting notes related to lean4#…

…1910, use new notation everywhere (#19369)

part 1: make applied occurances of `Additive.toAdd` and `Multiplicative.toMul` use newly available dot notation.



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -433,7 +433,7 @@ variable {G : Type*} [AddMonoid G] {a : G}
 as a monoid homomorphism from `Multiplicative G` to `G →+c[a, a] G`. -/
 @[simps! (config := .asFn)]
 def addLeftHom : Multiplicative G →* (G →+c[a, a] G) where
-  toFun c := Multiplicative.toAdd c +ᵥ .id
+  toFun c := c.toAdd +ᵥ .id
   map_one' := by ext; apply zero_add
   map_mul' _ _ := by ext; apply add_assoc
 

Mathlib/Algebra/AddTorsor.lean

@@ -358,7 +358,7 @@ theorem constVAdd_add (v₁ v₂ : G) : constVAdd P (v₁ + v₂) = constVAdd P
 
 /-- `Equiv.constVAdd` as a homomorphism from `Multiplicative G` to `Equiv.perm P` -/
 def constVAddHom : Multiplicative G →* Equiv.Perm P where
-  toFun v := constVAdd P (Multiplicative.toAdd v)
+  toFun v := constVAdd P (v.toAdd)
   map_one' := constVAdd_zero G P
   map_mul' := constVAdd_add P
 

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -2197,7 +2197,7 @@ variable [Monoid α]
 theorem ofMul_list_prod (s : List α) : ofMul s.prod = (s.map ofMul).sum := by simp [ofMul]; rfl
 
 @[simp]
-theorem toMul_list_sum (s : List (Additive α)) : toMul s.sum = (s.map toMul).prod := by
+theorem toMul_list_sum (s : List (Additive α)) : s.sum.toMul = (s.map toMul).prod := by
   simp [toMul, ofMul]; rfl
 
 end Monoid
@@ -2210,7 +2210,7 @@ variable [AddMonoid α]
 theorem ofAdd_list_prod (s : List α) : ofAdd s.sum = (s.map ofAdd).prod := by simp [ofAdd]; rfl
 
 @[simp]
-theorem toAdd_list_sum (s : List (Multiplicative α)) : toAdd s.prod = (s.map toAdd).sum := by
+theorem toAdd_list_sum (s : List (Multiplicative α)) : s.prod.toAdd = (s.map toAdd).sum := by
   simp [toAdd, ofAdd]; rfl
 
 end AddMonoid
@@ -2224,7 +2224,7 @@ theorem ofMul_multiset_prod (s : Multiset α) : ofMul s.prod = (s.map ofMul).sum
   simp [ofMul]; rfl
 
 @[simp]
-theorem toMul_multiset_sum (s : Multiset (Additive α)) : toMul s.sum = (s.map toMul).prod := by
+theorem toMul_multiset_sum (s : Multiset (Additive α)) : s.sum.toMul = (s.map toMul).prod := by
   simp [toMul, ofMul]; rfl
 
 @[simp]
@@ -2233,7 +2233,7 @@ theorem ofMul_prod (s : Finset ι) (f : ι → α) : ofMul (∏ i ∈ s, f i) =
 
 @[simp]
 theorem toMul_sum (s : Finset ι) (f : ι → Additive α) :
-    toMul (∑ i ∈ s, f i) = ∏ i ∈ s, toMul (f i) :=
+    (∑ i ∈ s, f i).toMul = ∏ i ∈ s, (f i).toMul :=
   rfl
 
 end CommMonoid
@@ -2248,7 +2248,7 @@ theorem ofAdd_multiset_prod (s : Multiset α) : ofAdd s.sum = (s.map ofAdd).prod
 
 @[simp]
 theorem toAdd_multiset_sum (s : Multiset (Multiplicative α)) :
-    toAdd s.prod = (s.map toAdd).sum := by
+    s.prod.toAdd = (s.map toAdd).sum := by
   simp [toAdd, ofAdd]; rfl
 
 @[simp]
@@ -2257,7 +2257,7 @@ theorem ofAdd_sum (s : Finset ι) (f : ι → α) : ofAdd (∑ i ∈ s, f i) = 
 
 @[simp]
 theorem toAdd_prod (s : Finset ι) (f : ι → Multiplicative α) :
-    toAdd (∏ i ∈ s, f i) = ∑ i ∈ s, toAdd (f i) :=
+    (∏ i ∈ s, f i).toAdd = ∑ i ∈ s, (f i).toAdd :=
   rfl
 
 end AddCommMonoid

Mathlib/Algebra/Group/Action/TypeTags.lean

@@ -24,15 +24,15 @@ section
 
 open Additive Multiplicative
 
-instance Additive.vadd [SMul α β] : VAdd (Additive α) β where vadd a := (toMul a • ·)
+instance Additive.vadd [SMul α β] : VAdd (Additive α) β where vadd a := (a.toMul • ·)
 
-instance Multiplicative.smul [VAdd α β] : SMul (Multiplicative α) β where smul a := (toAdd a +ᵥ ·)
+instance Multiplicative.smul [VAdd α β] : SMul (Multiplicative α) β where smul a := (a.toAdd +ᵥ ·)
 
-@[simp] lemma toMul_smul [SMul α β] (a) (b : β) : (toMul a : α) • b = a +ᵥ b := rfl
+@[simp] lemma toMul_smul [SMul α β] (a:Additive α) (b : β) : (a.toMul : α) • b = a +ᵥ b := rfl
 
 @[simp] lemma ofMul_vadd [SMul α β] (a : α) (b : β) : ofMul a +ᵥ b = a • b := rfl
 
-@[simp] lemma toAdd_vadd [VAdd α β] (a) (b : β) : (toAdd a : α) +ᵥ b = a • b := rfl
+@[simp] lemma toAdd_vadd [VAdd α β] (a:Multiplicative α) (b : β) : (a.toAdd : α) +ᵥ b = a • b := rfl
 
 @[simp] lemma ofAdd_smul [VAdd α β] (a : α) (b : β) : ofAdd a • b = a +ᵥ b := rfl
 

Mathlib/Algebra/Group/AddChar.lean

@@ -115,7 +115,7 @@ def toMonoidHom (φ : AddChar A M) : Multiplicative A →* M where
 -- this instance was a bad idea and conflicted with `instFunLike` above
 
 @[simp] lemma toMonoidHom_apply (ψ : AddChar A M) (a : Multiplicative A) :
-  ψ.toMonoidHom a = ψ (Multiplicative.toAdd a) :=
+  ψ.toMonoidHom a = ψ a.toAdd :=
   rfl
 
 /-- An additive character maps multiples by natural numbers to powers. -/
@@ -142,7 +142,7 @@ def toMonoidHomEquiv : AddChar A M ≃ (Multiplicative A →* M) where
     ⇑(toMonoidHomEquiv.symm ψ) = ψ ∘ Multiplicative.ofAdd := rfl
 
 @[simp] lemma toMonoidHomEquiv_apply (ψ : AddChar A M) (a : Multiplicative A) :
-    toMonoidHomEquiv ψ a = ψ (Multiplicative.toAdd a) := rfl
+    toMonoidHomEquiv ψ a = ψ a.toAdd := rfl
 
 @[simp] lemma toMonoidHomEquiv_symm_apply (ψ : Multiplicative A →* M) (a : A) :
     toMonoidHomEquiv.symm ψ a = ψ (Multiplicative.ofAdd a) := rfl
@@ -180,7 +180,7 @@ lemma coe_toAddMonoidHomEquiv (ψ : AddChar A M) :
     toAddMonoidHomEquiv ψ a = Additive.ofMul (ψ a) := rfl
 
 @[simp] lemma toAddMonoidHomEquiv_symm_apply (ψ : A →+ Additive M) (a : A) :
-    toAddMonoidHomEquiv.symm ψ a = Additive.toMul (ψ a) := rfl
+    toAddMonoidHomEquiv.symm ψ a = (ψ a).toMul  := rfl
 
 /-- The trivial additive character (sending everything to `1`). -/
 instance instOne : One (AddChar A M) := toMonoidHomEquiv.one

Mathlib/Algebra/Group/Aut.lean

@@ -260,9 +260,9 @@ theorem conj_symm_apply [AddGroup G] (g h : G) : (conj g).symm h = -g + h + g :=
 
 -- Porting note: the exact translation of this mathlib3 lemma would be`(-conj g) h = -g + h + g`,
 -- but this no longer pass the simp_nf linter, as the LHS simplifies by `toMul_neg` to
--- `(Additive.toMul (conj g))⁻¹`.
+-- `(conj g).toMul⁻¹`.
 @[simp]
-theorem conj_inv_apply [AddGroup G] (g h : G) : (Additive.toMul (conj g))⁻¹ h = -g + h + g :=
+theorem conj_inv_apply [AddGroup G] (g h : G) : (conj g).toMul⁻¹ h = -g + h + g :=
   rfl
 
 /-- Isomorphic additive groups have isomorphic automorphism groups. -/

Mathlib/Algebra/Group/Equiv/TypeTags.lean

@@ -118,8 +118,8 @@ and multiplicative endomorphisms of `Multiplicative A`. -/
 @[simps]
 def MulEquiv.piMultiplicative (K : ι → Type*) [∀ i, Add (K i)] :
     Multiplicative (∀ i : ι, K i) ≃* (∀ i : ι, Multiplicative (K i)) where
-  toFun x := fun i ↦ Multiplicative.ofAdd <| Multiplicative.toAdd x i
-  invFun x := Multiplicative.ofAdd fun i ↦ Multiplicative.toAdd (x i)
+  toFun x := fun i ↦ Multiplicative.ofAdd <| x.toAdd i
+  invFun x := Multiplicative.ofAdd fun i ↦ (x i).toAdd
   left_inv _ := rfl
   right_inv _ := rfl
   map_mul' _ _ := rfl
@@ -134,8 +134,8 @@ abbrev MulEquiv.funMultiplicative [Add G] :
 @[simps]
 def AddEquiv.piAdditive (K : ι → Type*) [∀ i, Mul (K i)] :
     Additive (∀ i : ι, K i) ≃+ (∀ i : ι, Additive (K i)) where
-  toFun x := fun i ↦ Additive.ofMul <| Additive.toMul x i
-  invFun x := Additive.ofMul fun i ↦ Additive.toMul (x i)
+  toFun x := fun i ↦ Additive.ofMul <| x.toMul i
+  invFun x := Additive.ofMul fun i ↦ (x i).toMul
   left_inv _ := rfl
   right_inv _ := rfl
   map_add' _ _ := rfl
@@ -164,9 +164,9 @@ def MulEquiv.multiplicativeAdditive [MulOneClass H] : Multiplicative (Additive H
 @[simps]
 def MulEquiv.prodMultiplicative [Add G] [Add H] :
     Multiplicative (G × H) ≃* Multiplicative G × Multiplicative H where
-  toFun x := (Multiplicative.ofAdd (Multiplicative.toAdd x).1,
-    Multiplicative.ofAdd (Multiplicative.toAdd x).2)
-  invFun := fun (x, y) ↦ Multiplicative.ofAdd (Multiplicative.toAdd x, Multiplicative.toAdd y)
+  toFun x := (Multiplicative.ofAdd x.toAdd.1,
+    Multiplicative.ofAdd x.toAdd.2)
+  invFun := fun (x, y) ↦ Multiplicative.ofAdd (x.toAdd, y.toAdd)
   left_inv _ := rfl
   right_inv _ := rfl
   map_mul' _ _ := rfl
@@ -175,9 +175,9 @@ def MulEquiv.prodMultiplicative [Add G] [Add H] :
 @[simps]
 def AddEquiv.prodAdditive [Mul G] [Mul H] :
     Additive (G × H) ≃+ Additive G × Additive H where
-  toFun x := (Additive.ofMul (Additive.toMul x).1,
-    Additive.ofMul (Additive.toMul x).2)
-  invFun := fun (x, y) ↦ Additive.ofMul (Additive.toMul x, Additive.toMul y)
+  toFun x := (Additive.ofMul x.toMul.1,
+    Additive.ofMul x.toMul.2)
+  invFun := fun (x, y) ↦ Additive.ofMul (x.toMul, y.toMul)
   left_inv _ := rfl
   right_inv _ := rfl
   map_add' _ _ := rfl

Mathlib/Algebra/Group/Even.lean

@@ -62,7 +62,7 @@ instance [DecidablePred (IsSquare : α → Prop)] : DecidablePred (IsSquare : α
 lemma even_ofMul_iff {a : α} : Even (Additive.ofMul a) ↔ IsSquare a := Iff.rfl
 
 @[simp]
-lemma isSquare_toMul_iff {a : Additive α} : IsSquare (Additive.toMul a) ↔ Even a := Iff.rfl
+lemma isSquare_toMul_iff {a : Additive α} : IsSquare (a.toMul) ↔ Even a := Iff.rfl
 
 instance Additive.instDecidablePredEven [DecidablePred (IsSquare : α → Prop)] :
     DecidablePred (Even : Additive α → Prop) :=
@@ -76,7 +76,7 @@ variable [Add α]
 @[simp] lemma isSquare_ofAdd_iff {a : α} : IsSquare (Multiplicative.ofAdd a) ↔ Even a := Iff.rfl
 
 @[simp]
-lemma even_toAdd_iff {a : Multiplicative α} : Even (Multiplicative.toAdd a) ↔ IsSquare a := Iff.rfl
+lemma even_toAdd_iff {a : Multiplicative α} : Even a.toAdd ↔ IsSquare a := Iff.rfl
 
 instance Multiplicative.instDecidablePredIsSquare [DecidablePred (Even : α → Prop)] :
     DecidablePred (IsSquare : Multiplicative α → Prop) :=

Mathlib/Algebra/Group/Int.lean

@@ -74,9 +74,9 @@ section Multiplicative
 
 open Multiplicative
 
-lemma toAdd_pow (a : Multiplicative ℤ) (b : ℕ) : toAdd (a ^ b) = toAdd a * b := mul_comm _ _
+lemma toAdd_pow (a : Multiplicative ℤ) (b : ℕ) : (a ^ b).toAdd = a.toAdd * b := mul_comm _ _
 
-lemma toAdd_zpow (a : Multiplicative ℤ) (b : ℤ) : toAdd (a ^ b) = toAdd a * b := mul_comm _ _
+lemma toAdd_zpow (a : Multiplicative ℤ) (b : ℤ) : (a ^ b).toAdd = a.toAdd * b := mul_comm _ _
 
 @[simp] lemma ofAdd_mul (a b : ℤ) : ofAdd (a * b) = ofAdd a ^ b := (toAdd_zpow ..).symm
 

Mathlib/Algebra/Group/Nat/TypeTags.lean

@@ -17,7 +17,7 @@ open Multiplicative
 
 namespace Nat
 
-lemma toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : toAdd (a ^ b) = toAdd a * b := mul_comm _ _
+lemma toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : (a ^ b).toAdd = a.toAdd * b := mul_comm _ _
 
 @[simp] lemma ofAdd_mul (a b : ℕ) : ofAdd (a * b) = ofAdd a ^ b := (toAdd_pow _ _).symm
 

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -475,7 +475,7 @@ when it is injective. The inverse is given by the logarithms. -/
 @[simps]
 def powLogEquiv [DecidableEq M] {n : M} (h : Function.Injective fun m : ℕ => n ^ m) :
     Multiplicative ℕ ≃* powers n where
-  toFun m := pow n (Multiplicative.toAdd m)
+  toFun m := pow n m.toAdd
   invFun m := Multiplicative.ofAdd (log m)
   left_inv := log_pow_eq_self h
   right_inv := pow_log_eq_self