feat(algebra/group/to_additive + a few more files): make to_additive convert unit to add_unit (#12564)

This likely involves removing names that match autogenerated names.



Co-authored-by: Alex J. Best <alex.j.best@gmail.com>

Author: adomani

src/algebra/group/to_additive.lean

@@ -225,6 +225,8 @@ meta def tr : bool → list string → list string
 | is_comm ("magma" :: s)       := ("add_" ++ add_comm_prefix is_comm "magma")     :: tr ff s
 | is_comm ("haar" :: s)        := ("add_" ++ add_comm_prefix is_comm "haar")      :: tr ff s
 | is_comm ("prehaar" :: s)     := ("add_" ++ add_comm_prefix is_comm "prehaar")   :: tr ff s
+| is_comm ("unit" :: s)        := ("add_" ++ add_comm_prefix is_comm "unit")      :: tr ff s
+| is_comm ("units" :: s)       := ("add_" ++ add_comm_prefix is_comm "units")     :: tr ff s
 | is_comm ("comm" :: s)        := tr tt s
 | is_comm (x :: s)             := (add_comm_prefix is_comm x :: tr ff s)
 | tt []                        := ["comm"]

src/algebra/group/units.lean

@@ -53,7 +53,7 @@ structure add_units (α : Type u) [add_monoid α] :=
 (val_neg : val + neg = 0)
 (neg_val : neg + val = 0)
 
-attribute [to_additive add_units] units
+attribute [to_additive] units
 
 section has_elem
 
@@ -278,12 +278,12 @@ variables {M : Type*} {N : Type*}
 /-- An element `a : M` of a monoid is a unit if it has a two-sided inverse.
 The actual definition says that `a` is equal to some `u : Mˣ`, where
 `Mˣ` is a bundled version of `is_unit`. -/
-@[to_additive is_add_unit "An element `a : M` of an add_monoid is an `add_unit` if it has
+@[to_additive "An element `a : M` of an add_monoid is an `add_unit` if it has
 a two-sided additive inverse. The actual definition says that `a` is equal to some
 `u : add_units M`, where `add_units M` is a bundled version of `is_add_unit`."]
 def is_unit [monoid M] (a : M) : Prop := ∃ u : Mˣ, (u : M) = a
 
-@[nontriviality, to_additive is_add_unit_of_subsingleton]
+@[nontriviality, to_additive]
 lemma is_unit_of_subsingleton [monoid M] [subsingleton M] (a : M) : is_unit a :=
 ⟨⟨a, a, subsingleton.elim _ _, subsingleton.elim _ _⟩, rfl⟩
 
@@ -301,10 +301,10 @@ attribute [nontriviality] is_add_unit_of_subsingleton
 @[simp, to_additive is_add_unit_add_unit]
 protected lemma units.is_unit [monoid M] (u : Mˣ) : is_unit (u : M) := ⟨u, rfl⟩
 
-@[simp, to_additive is_add_unit_zero]
+@[simp, to_additive]
 theorem is_unit_one [monoid M] : is_unit (1:M) := ⟨1, rfl⟩
 
-@[to_additive is_add_unit_of_add_eq_zero] theorem is_unit_of_mul_eq_one [comm_monoid M]
+@[to_additive] theorem is_unit_of_mul_eq_one [comm_monoid M]
   (a b : M) (h : a * b = 1) : is_unit a :=
 ⟨units.mk_of_mul_eq_one a b h, rfl⟩
 
@@ -316,12 +316,12 @@ by { rcases h with ⟨⟨a, b, hab, _⟩, rfl⟩, exact ⟨b, hab⟩ }
   {a : M} (h : is_unit a) : ∃ b, b * a = 1 :=
 by { rcases h with ⟨⟨a, b, _, hba⟩, rfl⟩, exact ⟨b, hba⟩ }
 
-@[to_additive is_add_unit_iff_exists_neg] theorem is_unit_iff_exists_inv [comm_monoid M]
+@[to_additive] theorem is_unit_iff_exists_inv [comm_monoid M]
   {a : M} : is_unit a ↔ ∃ b, a * b = 1 :=
 ⟨λ h, h.exists_right_inv,
  λ ⟨b, hab⟩, is_unit_of_mul_eq_one _ b hab⟩
 
-@[to_additive is_add_unit_iff_exists_neg'] theorem is_unit_iff_exists_inv' [comm_monoid M]
+@[to_additive] theorem is_unit_iff_exists_inv' [comm_monoid M]
   {a : M} : is_unit a ↔ ∃ b, b * a = 1 :=
 by simp [is_unit_iff_exists_inv, mul_comm]
 
@@ -330,7 +330,7 @@ lemma is_unit.mul [monoid M] {x y : M} : is_unit x → is_unit y → is_unit (x
 by { rintros ⟨x, rfl⟩ ⟨y, rfl⟩, exact ⟨x * y, units.coe_mul _ _⟩ }
 
 /-- Multiplication by a `u : Mˣ` on the right doesn't affect `is_unit`. -/
-@[simp, to_additive is_add_unit_add_add_units "Addition of a `u : add_units M` on the right doesn't
+@[simp, to_additive "Addition of a `u : add_units M` on the right doesn't
 affect `is_add_unit`."]
 theorem units.is_unit_mul_units [monoid M] (a : M) (u : Mˣ) :
   is_unit (a * u) ↔ is_unit a :=
@@ -341,8 +341,7 @@ iff.intro
   (λ v, v.mul u.is_unit)
 
 /-- Multiplication by a `u : Mˣ` on the left doesn't affect `is_unit`. -/
-@[simp, to_additive is_add_unit_add_units_add "Addition of a `u : add_units M` on the left doesn't
-affect `is_add_unit`."]
+@[simp, to_additive "Addition of a `u : add_units M` on the left doesn't affect `is_add_unit`."]
 theorem units.is_unit_units_mul {M : Type*} [monoid M] (u : Mˣ) (a : M) :
   is_unit (↑u * a) ↔ is_unit a :=
 iff.intro
@@ -351,7 +350,7 @@ iff.intro
     by rwa [←mul_assoc, units.inv_mul, one_mul] at this)
   u.is_unit.mul
 
-@[to_additive is_add_unit_of_add_is_add_unit_left]
+@[to_additive]
 theorem is_unit_of_mul_is_unit_left [comm_monoid M] {x y : M}
   (hu : is_unit (x * y)) : is_unit x :=
 let ⟨z, hz⟩ := is_unit_iff_exists_inv.1 hu in

src/data/equiv/mul_add.lean

@@ -476,18 +476,18 @@ def monoid_hom.to_mul_equiv [mul_one_class M] [mul_one_class N] (f : M →* N) (
   map_mul' := f.map_mul }
 
 /-- A group is isomorphic to its group of units. -/
-@[to_additive to_add_units "An additive group is isomorphic to its group of additive units"]
+@[to_additive "An additive group is isomorphic to its group of additive units"]
 def to_units [group G] : G ≃* Gˣ :=
 { to_fun := λ x, ⟨x, x⁻¹, mul_inv_self _, inv_mul_self _⟩,
   inv_fun := coe,
   left_inv := λ x, rfl,
   right_inv := λ u, units.ext rfl,
   map_mul' := λ x y, units.ext rfl }
 
-@[simp, to_additive coe_to_add_units] lemma coe_to_units [group G] (g : G) :
+@[simp, to_additive] lemma coe_to_units [group G] (g : G) :
   (to_units g : G) = g := rfl
 
-@[to_additive add_group.is_add_unit]
+@[to_additive]
 protected lemma group.is_unit {G} [group G] (x : G) : is_unit x := (to_units x).is_unit
 
 namespace units

src/group_theory/congruence.lean

@@ -985,7 +985,7 @@ variables {α : Type*} [monoid M] {c : con M}
 where `c : con M` is a multiplicative congruence on a monoid, it suffices to define a function `f`
 that takes elements `x y : M` with proofs of `c (x * y) 1` and `c (y * x) 1`, and returns an element
 of `α` provided that `f x y _ _ = f x' y' _ _` whenever `c x x'` and `c y y'`. -/
-@[to_additive lift_on_add_units] def lift_on_units (u : units c.quotient)
+@[to_additive] def lift_on_units (u : units c.quotient)
   (f : Π (x y : M), c (x * y) 1 → c (y * x) 1 → α)
   (Hf : ∀ x y hxy hyx x' y' hxy' hyx', c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx') :
   α :=
@@ -1014,7 +1014,7 @@ lemma lift_on_units_mk (f : Π (x y : M), c (x * y) 1 → c (y * x) 1 → α)
   lift_on_units ⟨(x : c.quotient), y, hxy, hyx⟩ f Hf = f x y (c.eq.1 hxy) (c.eq.1 hyx) :=
 rfl
 
-@[elab_as_eliminator, to_additive induction_on_add_units]
+@[elab_as_eliminator, to_additive]
 lemma induction_on_units {p : units c.quotient → Prop} (u : units c.quotient)
   (H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p ⟨x, y, c.eq.2 hxy, c.eq.2 hyx⟩) :
   p u :=

src/group_theory/order_of_element.lean

@@ -207,7 +207,7 @@ by simp_rw [order_of_eq_order_of_iff, ←f.map_pow, ←f.map_one, hf.eq_iff, iff
   (y : H) : order_of (y : G) = order_of y :=
 order_of_injective H.subtype subtype.coe_injective y
 
-@[to_additive order_of_add_units]
+@[to_additive]
 lemma order_of_units {y : Gˣ} : order_of (y : G) = order_of y :=
 order_of_injective (units.coe_hom G) units.ext y