From 4e5518cafc0efd7c7b7d287fa960fce5201908db Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 4 Nov 2023 02:30:05 +0000 Subject: [PATCH] feat: rewrite lemma for `Monoid.exponent (Multiplicative G)` (#8093) This also fixes a `to_additive` naming error --- Mathlib/GroupTheory/Exponent.lean | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/Mathlib/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean index afcb06c881f5a..988880b6a5f87 100644 --- a/Mathlib/GroupTheory/Exponent.lean +++ b/Mathlib/GroupTheory/Exponent.lean @@ -80,6 +80,21 @@ noncomputable def exponent := variable {G} +@[simp] +theorem _root_.AddMonoid.exponent_additive : + AddMonoid.exponent (Additive G) = exponent G := rfl + +@[simp] +theorem exponent_multiplicative {G : Type*} [AddMonoid G] : + exponent (Multiplicative G) = AddMonoid.exponent G := rfl + +open MulOpposite in +@[to_additive (attr := simp)] +theorem _root_.MulOpposite.exponent : exponent (MulOpposite G) = exponent G := by + simp only [Monoid.exponent, ExponentExists] + congr! + all_goals exact ⟨(op_injective <| · <| op ·), (unop_injective <| . <| unop .)⟩ + @[to_additive] theorem exponentExists_iff_ne_zero : ExponentExists G ↔ exponent G ≠ 0 := by rw [exponent] @@ -432,8 +447,8 @@ theorem Monoid.exponent_pi {ι : Type*} [Fintype ι] {M : ι → Type*} [∀ i, /-- The exponent of product of two monoids is the `lcm` of the exponents of the individuaul monoids. -/ -@[to_additive "The exponent of product of two additive monoids is the `lcm` of the exponents of the -individuaul additive monoids."] +@[to_additive AddMonoid.exponent_prod "The exponent of product of two additive monoids is the `lcm` +of the exponents of the individuaul additive monoids."] theorem Monoid.exponent_prod {M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂] : exponent (M₁ × M₂) = lcm (exponent M₁) (exponent M₂) := by refine dvd_antisymm ?_ (lcm_dvd ?_ ?_)