From 9c15e5fa359a9c13d086cf5e5279b2be7d298399 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 10 Dec 2024 22:09:36 -0800 Subject: [PATCH 1/3] chore: rename `DivInvMonoid.Pow` This didn't match the naming convention at all. Loogle tells me that `ZPow` is slightly more common than `PowInt`, though both are used. This is an instance, so the name needs no deprecation --- Mathlib/Algebra/Group/Defs.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 3d069aab663a3..8a7241723a8a5 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -858,13 +858,13 @@ class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where attribute [to_additive SubNegMonoid] DivInvMonoid -instance DivInvMonoid.Pow {M} [DivInvMonoid M] : Pow M ℤ := +instance DivInvMonoid.toZPow {M} [DivInvMonoid M] : Pow M ℤ := ⟨fun x n ↦ DivInvMonoid.zpow n x⟩ -instance SubNegMonoid.SMulInt {M} [SubNegMonoid M] : SMul ℤ M := +instance SubNegMonoid.toZSMul {M} [SubNegMonoid M] : SMul ℤ M := ⟨SubNegMonoid.zsmul⟩ -attribute [to_additive existing SubNegMonoid.SMulInt] DivInvMonoid.Pow +attribute [to_additive existing SubNegMonoid.toZSMul] DivInvMonoid.toZPow /-- A group is called *cyclic* if it is generated by a single element. -/ class IsAddCyclic (G : Type u) [SMul ℤ G] : Prop where From 6c54764eefb568f38a067d2f621d21f84bbf420c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 10 Dec 2024 23:35:52 -0800 Subject: [PATCH 2/3] Update Defs.lean --- Mathlib/Algebra/Group/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index 8a7241723a8a5..394c147b9bf64 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -864,7 +864,7 @@ instance DivInvMonoid.toZPow {M} [DivInvMonoid M] : Pow M ℤ := instance SubNegMonoid.toZSMul {M} [SubNegMonoid M] : SMul ℤ M := ⟨SubNegMonoid.zsmul⟩ -attribute [to_additive existing SubNegMonoid.toZSMul] DivInvMonoid.toZPow +attribute [to_additive existing] DivInvMonoid.toZPow /-- A group is called *cyclic* if it is generated by a single element. -/ class IsAddCyclic (G : Type u) [SMul ℤ G] : Prop where From e3ac7530badbee76f476ef28a69de38aecadda34 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 11 Dec 2024 00:58:57 -0800 Subject: [PATCH 3/3] Update IntUnitsPower.lean --- Mathlib/Data/ZMod/IntUnitsPower.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/ZMod/IntUnitsPower.lean b/Mathlib/Data/ZMod/IntUnitsPower.lean index 4b5cace9f38cd..61cc3341fdfc7 100644 --- a/Mathlib/Data/ZMod/IntUnitsPower.lean +++ b/Mathlib/Data/ZMod/IntUnitsPower.lean @@ -60,7 +60,7 @@ instance Int.instUnitsPow : Pow ℤˣ R where -- The above instances form no typeclass diamonds with the standard power operators -- but we will need `reducible_and_instances` which currently fails https://github.com/leanprover-community/mathlib4/issues/10906 example : Int.instUnitsPow = Monoid.toNatPow := rfl -example : Int.instUnitsPow = DivInvMonoid.Pow := rfl +example : Int.instUnitsPow = DivInvMonoid.toZPow := rfl @[simp] lemma ofMul_uzpow (u : ℤˣ) (r : R) : Additive.ofMul (u ^ r) = r • Additive.ofMul u := rfl