From 84cbbc986431e150ee6f5ab98a734c16e10fe2ad Mon Sep 17 00:00:00 2001 From: damiano Date: Thu, 10 Mar 2022 21:17:59 +0000 Subject: [PATCH] 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 --- src/algebra/group/to_additive.lean | 2 ++ src/algebra/group/units.lean | 21 ++++++++++----------- src/data/equiv/mul_add.lean | 6 +++--- src/group_theory/congruence.lean | 4 ++-- src/group_theory/order_of_element.lean | 2 +- 5 files changed, 18 insertions(+), 17 deletions(-) diff --git a/src/algebra/group/to_additive.lean b/src/algebra/group/to_additive.lean index 201eeb8421a72..cbff37c3b5385 100644 --- a/src/algebra/group/to_additive.lean +++ b/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"] diff --git a/src/algebra/group/units.lean b/src/algebra/group/units.lean index 067809ddbd65a..e290396cacf7f 100644 --- a/src/algebra/group/units.lean +++ b/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 diff --git a/src/data/equiv/mul_add.lean b/src/data/equiv/mul_add.lean index 7f744d5be3226..954813b0c8887 100644 --- a/src/data/equiv/mul_add.lean +++ b/src/data/equiv/mul_add.lean @@ -476,7 +476,7 @@ 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, @@ -484,10 +484,10 @@ def to_units [group G] : G ≃* Gˣ := 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 diff --git a/src/group_theory/congruence.lean b/src/group_theory/congruence.lean index 4ca45b76de621..fa606333cb760 100644 --- a/src/group_theory/congruence.lean +++ b/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 := diff --git a/src/group_theory/order_of_element.lean b/src/group_theory/order_of_element.lean index 452a33568b5e2..9beeb7a6a77b4 100644 --- a/src/group_theory/order_of_element.lean +++ b/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