Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Neil Strickland, Yury Kudryashov

! This file was ported from Lean 3 source module algebra.group.commute
! leanprover-community/mathlib commit 05101c3df9d9cfe9430edc205860c79b6d660102
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Semiconj

/-!
# Commuting pairs of elements in monoids

We define the predicate `Commute a b := a * b = b * a` and provide some operations on terms
`(h : Commute a b)`. E.g., if `a`, `b`, and c are elements of a semiring, and that
`hb : Commute a b` and `hc : Commute a c`.  Then `hb.pow_left 5` proves `Commute (a ^ 5) b` and
`(hb.pow_right 2).add_right (hb.mul_right hc)` proves `Commute a (b ^ 2 + b * c)`.

Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like
`rw [(hb.pow_left 5).eq]` rather than just `rw [hb.pow_left 5]`.

This file defines only a few operations (`mul_left`, `inv_right`, etc).  Other operations
(`pow_right`, field inverse etc) are in the files that define corresponding notions.

## Implementation details

Most of the proofs come from the properties of `SemiconjBy`.
-/

variable {G: Type ?u.5G : Type _: Type (?u.5636+1)Type _}

/-- Two elements commute if `a * b = b * a`. -/
@[to_additive AddCommute: {S : Type u_1} β [inst : Add S] β S β S β PropAddCommute "Two elements additively commute if `a + b = b + a`"]
def Commute: {S : Type u_1} β [inst : Mul S] β S β S β PropCommute {S: Type ?u.8S : Type _: Type (?u.8+1)Type _} [Mul: Type ?u.11 β Type ?u.11Mul S: Type ?u.8S] (a: Sa b: Sb : S: Type ?u.8S) : Prop: TypeProp :=
SemiconjBy: {M : Type ?u.23} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Sa b: Sb b: Sb
#align commute Commute: {S : Type u_1} β [inst : Mul S] β S β S β PropCommute

namespace Commute

section Mul

variable {S: Type ?u.194S : Type _: Type (?u.403+1)Type _} [Mul: Type ?u.69 β Type ?u.69Mul S: Type ?u.66S]

/-- Equality behind `Commute a b`; useful for rewriting. -/
@[to_additive: β {S : Type u_1} [inst : Add S] {a b : S}, AddCommute a b β a + b = b + ato_additive "Equality behind `add_commute a b`; useful for rewriting."]
protected theorem eq: β {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq {a: Sa b: Sb : S: Type ?u.75S} (h: Commute a bh : Commute: {S : Type ?u.85} β [inst : Mul S] β S β S β PropCommute a: Sa b: Sb) : a: Sa * b: Sb = b: Sb * a: Sa :=
h: Commute a bh
#align commute.eq Commute.eq: β {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aCommute.eq

/-- Any element commutes with itself. -/
@[to_additive: β {S : Type u_1} [inst : Add S] (a : S), AddCommute a ato_additive (attr := refl, simp) "Any element commutes with itself."]
protected theorem refl: β (a : S), Commute a arefl (a: Sa : S: Type ?u.194S) : Commute: {S : Type ?u.202} β [inst : Mul S] β S β S β PropCommute a: Sa a: Sa :=
Eq.refl: β {Ξ± : Sort ?u.217} (a : Ξ±), a = aEq.refl (a: Sa * a: Sa)
#align commute.refl Commute.refl: β {S : Type u_1} [inst : Mul S] (a : S), Commute a aCommute.refl

/-- If `a` commutes with `b`, then `b` commutes with `a`. -/
@[to_additive: β {S : Type u_1} [inst : Add S] {a b : S}, AddCommute a b β AddCommute b ato_additive (attr := symm) "If `a` commutes with `b`, then `b` commutes with `a`."]
protected theorem symm: β {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b β Commute b asymm {a: Sa b: Sb : S: Type ?u.315S} (h: Commute a bh : Commute: {S : Type ?u.325} β [inst : Mul S] β S β S β PropCommute a: Sa b: Sb) : Commute: {S : Type ?u.339} β [inst : Mul S] β S β S β PropCommute b: Sb a: Sa :=
Eq.symm: β {Ξ± : Sort ?u.353} {a b : Ξ±}, a = b β b = aEq.symm h: Commute a bh
#align commute.symm Commute.symm: β {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b β Commute b aCommute.symm

protected theorem semiconjBy: β {a b : S}, Commute a b β SemiconjBy a b bsemiconjBy {a: Sa b: Sb : S: Type ?u.403S} (h: Commute a bh : Commute: {S : Type ?u.413} β [inst : Mul S] β S β S β PropCommute a: Sa b: Sb) : SemiconjBy: {M : Type ?u.427} β [inst : Mul M] β M β M β M β PropSemiconjBy a: Sa b: Sb b: Sb :=
h: Commute a bh
#align commute.semiconj_by Commute.semiconjBy: β {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b β SemiconjBy a b bCommute.semiconjBy

protected theorem symm_iff: β {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b β Commute b asymm_iff {a: Sa b: Sb : S: Type ?u.470S} : Commute: {S : Type ?u.480} β [inst : Mul S] β S β S β PropCommute a: Sa b: Sb β Commute: {S : Type ?u.488} β [inst : Mul S] β S β S β PropCommute b: Sb a: Sa :=
β¨Commute.symm: β {S : Type ?u.502} [inst : Mul S] {a b : S}, Commute a b β Commute b aCommute.symm, Commute.symm: β {S : Type ?u.523} [inst : Mul S] {a b : S}, Commute a b β Commute b aCommute.symmβ©
#align commute.symm_iff Commute.symm_iff: β {S : Type u_1} [inst : Mul S] {a b : S}, Commute a b β Commute b aCommute.symm_iff

instance: β {S : Type u_1} [inst : Mul S], IsRefl S Commuteinstance : IsRefl: (Ξ± : Type ?u.565) β (Ξ± β Ξ± β Prop) β PropIsRefl S: Type ?u.559S Commute: {S : Type ?u.566} β [inst : Mul S] β S β S β PropCommute :=
β¨Commute.refl: β {S : Type ?u.597} [inst : Mul S] (a : S), Commute a aCommute.reflβ©

-- This instance is useful for `Finset.noncomm_prod`
@[to_additive: β {G : Type u_1} {S : Type u_2} [inst : Add S] {f : G β S}, IsRefl G fun a b => AddCommute (f a) (f b)to_additive]
instance on_isRefl: β {f : G β S}, IsRefl G fun a b => Commute (f a) (f b)on_isRefl {f: G β Sf : G: Type ?u.656G β S: Type ?u.659S} : IsRefl: (Ξ± : Type ?u.669) β (Ξ± β Ξ± β Prop) β PropIsRefl G: Type ?u.656G fun a: ?m.671a b: ?m.674b => Commute: {S : Type ?u.676} β [inst : Mul S] β S β S β PropCommute (f: G β Sf a: ?m.671a) (f: G β Sf b: ?m.674b) :=
β¨fun _: ?m.705_ => Commute.refl: β {S : Type ?u.707} [inst : Mul S] (a : S), Commute a aCommute.refl _: ?m.708_β©
#align commute.on_is_refl Commute.on_isRefl: β {G : Type u_1} {S : Type u_2} [inst : Mul S] {f : G β S}, IsRefl G fun a b => Commute (f a) (f b)Commute.on_isRefl
#align add_commute.on_is_refl AddCommute.on_isRefl: β {G : Type u_1} {S : Type u_2} [inst : Add S] {f : G β S}, IsRefl G fun a b => AddCommute (f a) (f b)AddCommute.on_isRefl

end Mul

section Semigroup

variable {S: Type ?u.806S : Type _: Type (?u.1763+1)Type _} [Semigroup: Type ?u.809 β Type ?u.809Semigroup S: Type ?u.806S] {a: Sa b: Sb c: Sc : S: Type ?u.806S}

/-- If `a` commutes with both `b` and `c`, then it commutes with their product. -/
"If `a` commutes with both `b` and `c`, then it commutes with their sum."]
theorem mul_right: β {S : Type u_1} [inst : Semigroup S] {a b c : S}, Commute a b β Commute a c β Commute a (b * c)mul_right (hab: Commute a bhab : Commute: {S : Type ?u.833} β [inst : Mul S] β S β S β PropCommute a: Sa b: Sb) (hac: Commute a chac : Commute: {S : Type ?u.948} β [inst : Mul S] β S β S β PropCommute a: Sa c: Sc) : Commute: {S : Type ?u.957} β [inst : Mul S] β S β S β PropCommute a: Sa (b: Sb * c: Sc) :=
SemiconjBy.mul_right: β {S : Type ?u.1153} [inst : Semigroup S] {a x y x' y' : S},
SemiconjBy a x y β SemiconjBy a x' y' β SemiconjBy a (x * x') (y * y')SemiconjBy.mul_right hab: Commute a bhab hac: Commute a chac
#align commute.mul_right Commute.mul_rightβ: β {S : Type u_1} [inst : Semigroup S] {a b c : S}, Commute a b β Commute a c β Commute a (b * c)Commute.mul_rightβ
-- I think `β` is necessary because of the `mul` vs `HMul` distinction

/-- If both `a` and `b` commute with `c`, then their product commutes with `c`. -/
"If both `a` and `b` commute with `c`, then their product commutes with `c`."]
theorem mul_left: β {S : Type u_1} [inst : Semigroup S] {a b c : S}, Commute a c β Commute b c β Commute (a * b) cmul_left (hac: Commute a chac : Commute: {S : Type ?u.1304} β [inst : Mul S] β S β S β PropCommute a: Sa c: Sc) (hbc: Commute b chbc : Commute: {S : Type ?u.1419} β [inst : Mul S] β S β S β PropCommute b: Sb c: Sc) : Commute: {S : Type ?u.1428} β [inst : Mul S] β S β S β PropCommute (a: Sa * b: Sb) c: Sc :=
SemiconjBy.mul_left: β {S : Type ?u.1624} [inst : Semigroup S] {a b x y z : S}, SemiconjBy a y z β SemiconjBy b x y β SemiconjBy (a * b) x zSemiconjBy.mul_left hac: Commute a chac hbc: Commute b chbc
#align commute.mul_left Commute.mul_leftβ: β {S : Type u_1} [inst : Semigroup S] {a b c : S}, Commute a c β Commute b c β Commute (a * b) cCommute.mul_leftβ
-- I think `β` is necessary because of the `mul` vs `HMul` distinction

@[to_additive: β {S : Type u_1} [inst : AddSemigroup S] {b c : S}, AddCommute b c β β (a : S), a + b + c = a + c + bto_additive]
protected theorem right_comm: Commute b c β β (a : S), a * b * c = a * c * bright_comm (h: Commute b ch : Commute: {S : Type ?u.1775} β [inst : Mul S] β S β S β PropCommute b: Sb c: Sc) (a: Sa : S: Type ?u.1763S) : a: Sa * b: Sb * c: Sc = a: Sa * c: Sc * b: Sb :=
byGoals accomplished! π G: Type ?u.1760S: Type u_1instβ: Semigroup Saβ, b, c: Sh: Commute b ca: Sa * b * c = a * c * bsimp only [mul_assoc: β {G : Type ?u.2385} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc, h: Commute b ch.eq: β {S : Type ?u.2404} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq]Goals accomplished! π
#align commute.right_comm Commute.right_commβ: β {S : Type u_1} [inst : Semigroup S] {b c : S}, Commute b c β β (a : S), a * b * c = a * c * bCommute.right_commβ
#align add_commute.right_comm AddCommute.right_commβ: β {S : Type u_1} [inst : AddSemigroup S] {b c : S}, AddCommute b c β β (a : S), a + b + c = a + c + bAddCommute.right_commβ
-- I think `β` is necessary because of the `mul` vs `HMul` distinction

@[to_additive: β {S : Type u_1} [inst : AddSemigroup S] {a b : S}, AddCommute a b β β (c : S), a + (b + c) = b + (a + c)to_additive]
protected theorem left_comm: Commute a b β β (c : S), a * (b * c) = b * (a * c)left_comm (h: Commute a bh : Commute: {S : Type ?u.2646} β [inst : Mul S] β S β S β PropCommute a: Sa b: Sb) (c: ?m.2761c) : a: Sa * (b: Sb * c: ?m.2761c) = b: Sb * (a: Sa * c: ?m.2761c) :=
byGoals accomplished! π G: Type ?u.2631S: Type u_1instβ: Semigroup Sa, b, cβ: Sh: Commute a bc: Sa * (b * c) = b * (a * c)simp only [β mul_assoc: β {G : Type ?u.3257} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc, h: Commute a bh.eq: β {S : Type ?u.3281} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq]Goals accomplished! π
#align commute.left_comm Commute.left_commβ: β {S : Type u_1} [inst : Semigroup S] {a b : S}, Commute a b β β (c : S), a * (b * c) = b * (a * c)Commute.left_commβ
#align add_commute.left_comm AddCommute.left_commβ: β {S : Type u_1} [inst : AddSemigroup S] {a b : S}, AddCommute a b β β (c : S), a + (b + c) = b + (a + c)AddCommute.left_commβ
-- I think `β` is necessary because of the `mul` vs `HMul` distinction

@[to_additive: β {S : Type u_1} [inst : AddSemigroup S] {b c : S}, AddCommute b c β β (a d : S), a + b + (c + d) = a + c + (b + d)to_additive]
protected theorem mul_mul_mul_comm: Commute b c β β (a d : S), a * b * (c * d) = a * c * (b * d)mul_mul_mul_comm (hbc: Commute b chbc : Commute: {S : Type ?u.3544} β [inst : Mul S] β S β S β PropCommute b: Sb c: Sc) (a: Sa d: Sd : S: Type ?u.3532S) :
a: Sa * b: Sb * (c: Sc * d: Sd) = a: Sa * c: Sc * (b: Sb * d: Sd) := byGoals accomplished! π G: Type ?u.3529S: Type u_1instβ: Semigroup Saβ, b, c: Shbc: Commute b ca, d: Sa * b * (c * d) = a * c * (b * d)simp only [hbc: Commute b chbc.left_comm: β {S : Type ?u.4352} [inst : Semigroup S] {a b : S}, Commute a b β β (c : S), a * (b * c) = b * (a * c)left_comm, mul_assoc: β {G : Type ?u.4382} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc]Goals accomplished! π
#align commute.mul_mul_mul_comm Commute.mul_mul_mul_comm: β {S : Type u_1} [inst : Semigroup S] {b c : S}, Commute b c β β (a d : S), a * b * (c * d) = a * c * (b * d)Commute.mul_mul_mul_comm

end Semigroup

protected theorem all: β {S : Type u_1} [inst : CommSemigroup S] (a b : S), Commute a ball {S: Type ?u.4513S : Type _: Type (?u.4513+1)Type _} [CommSemigroup: Type ?u.4516 β Type ?u.4516CommSemigroup S: Type ?u.4513S] (a: Sa b: Sb : S: Type ?u.4513S) : Commute: {S : Type ?u.4523} β [inst : Mul S] β S β S β PropCommute a: Sa b: Sb :=
mul_comm: β {G : Type ?u.4666} [inst : CommSemigroup G] (a b : G), a * b = b * amul_comm a: Sa b: Sb
#align commute.all Commute.allβ: β {S : Type u_1} [inst : CommSemigroup S] (a b : S), Commute a bCommute.allβ
-- not sure why this needs an `β`, maybe instance names not aligned?

section MulOneClass

variable {M: Type ?u.4705M : Type _: Type (?u.4705+1)Type _} [MulOneClass: Type ?u.4708 β Type ?u.4708MulOneClass M: Type ?u.4705M]

theorem one_right: β (a : M), Commute a 1one_right (a: Ma : M: Type ?u.4705M) : Commute: {S : Type ?u.4713} β [inst : Mul S] β S β S β PropCommute a: Ma 1: ?m.47211 :=
SemiconjBy.one_right: β {M : Type ?u.4854} [inst : MulOneClass M] (a : M), SemiconjBy a 1 1SemiconjBy.one_right a: Ma
#align commute.one_right Commute.one_rightβ: β {M : Type u_1} [inst : MulOneClass M] (a : M), Commute a 1Commute.one_rightβ
-- I think `β` is necessary because `One.toOfNat1` appears in the Lean 4 version

theorem one_left: β {M : Type u_1} [inst : MulOneClass M] (a : M), Commute 1 aone_left (a: Ma : M: Type ?u.4914M) : Commute: {S : Type ?u.4922} β [inst : Mul S] β S β S β PropCommute 1: ?m.49301 a: Ma :=
SemiconjBy.one_left: β {M : Type ?u.5069} [inst : MulOneClass M] (x : M), SemiconjBy 1 x xSemiconjBy.one_left a: Ma
#align commute.one_left Commute.one_leftβ: β {M : Type u_1} [inst : MulOneClass M] (a : M), Commute 1 aCommute.one_leftβ
-- I think `β` is necessary because `One.toOfNat1` appears in the Lean 4 version

end MulOneClass

section Monoid

variable {M: Type ?u.5129M : Type _: Type (?u.8434+1)Type _} [Monoid: Type ?u.7760 β Type ?u.7760Monoid M: Type ?u.9814M] {a: Ma b: Mb : M: Type ?u.6153M} {u: MΛ£u uβ: MΛ£uβ uβ: MΛ£uβ : M: Type ?u.5129MΛ£}

@[to_additive: β {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b β β (n : β), AddCommute a (n β’ b)to_additive (attr := simp)]
theorem pow_right: β {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b β β (n : β), Commute a (b ^ n)pow_right (h: Commute a bh : Commute: {S : Type ?u.5190} β [inst : Mul S] β S β S β PropCommute a: Ma b: Mb) (n: βn : β: Typeβ) : Commute: {S : Type ?u.5220} β [inst : Mul S] β S β S β PropCommute a: Ma (b: Mb ^ n: βn) :=
SemiconjBy.pow_right: β {M : Type ?u.5523} [inst : Monoid M] {a x y : M}, SemiconjBy a x y β β (n : β), SemiconjBy a (x ^ n) (y ^ n)SemiconjBy.pow_right h: Commute a bh n: βn
#align commute.pow_right Commute.pow_rightβ: β {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b β β (n : β), Commute a (b ^ n)Commute.pow_rightβ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

@[to_additive: β {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b β β (n : β), AddCommute (n β’ a) bto_additive (attr := simp)]
theorem pow_left: Commute a b β β (n : β), Commute (a ^ n) bpow_left (h: Commute a bh : Commute: {S : Type ?u.5668} β [inst : Mul S] β S β S β PropCommute a: Ma b: Mb) (n: βn : β: Typeβ) : Commute: {S : Type ?u.5698} β [inst : Mul S] β S β S β PropCommute (a: Ma ^ n: βn) b: Mb :=
(h: Commute a bh.symm: β {S : Type ?u.6001} [inst : Mul S] {a b : S}, Commute a b β Commute b asymm.pow_right: β {M : Type ?u.6029} [inst : Monoid M] {a b : M}, Commute a b β β (n : β), Commute a (b ^ n)pow_right n: βn).symm: β {S : Type ?u.6051} [inst : Mul S] {a b : S}, Commute a b β Commute b asymm
#align commute.pow_left Commute.pow_leftβ: β {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b β β (n : β), Commute (a ^ n) bCommute.pow_leftβ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

-- todo: should nat power be called `nsmul` here?
@[to_additive: β {M : Type u_1} [inst : AddMonoid M] {a b : M}, AddCommute a b β β (m n : β), AddCommute (m β’ a) (n β’ b)to_additive (attr := simp)]
theorem pow_pow: Commute a b β β (m n : β), Commute (a ^ m) (b ^ n)pow_pow (h: Commute a bh : Commute: {S : Type ?u.6182} β [inst : Mul S] β S β S β PropCommute a: Ma b: Mb) (m: βm n: βn : β: Typeβ) : Commute: {S : Type ?u.6214} β [inst : Mul S] β S β S β PropCommute (a: Ma ^ m: βm) (b: Mb ^ n: βn) :=
(h: Commute a bh.pow_left: β {M : Type ?u.6759} [inst : Monoid M] {a b : M}, Commute a b β β (n : β), Commute (a ^ n) bpow_left m: βm).pow_right: β {M : Type ?u.6787} [inst : Monoid M] {a b : M}, Commute a b β β (n : β), Commute a (b ^ n)pow_right n: βn
#align commute.pow_pow Commute.pow_powβ: β {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b β β (m n : β), Commute (a ^ m) (b ^ n)Commute.pow_powβ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

-- porting note: `simpNF` told me to remove the `simp` attribute
theorem self_pow: β {M : Type u_1} [inst : Monoid M] (a : M) (n : β), Commute a (a ^ n)self_pow (a: Ma : M: Type ?u.6903M) (n: βn : β: Typeβ) : Commute: {S : Type ?u.6936} β [inst : Mul S] β S β S β PropCommute a: Ma (a: Ma ^ n: βn) :=
(Commute.refl: β {S : Type ?u.7258} [inst : Mul S] (a : S), Commute a aCommute.refl a: Ma).pow_right: β {M : Type ?u.7280} [inst : Monoid M] {a b : M}, Commute a b β β (n : β), Commute a (b ^ n)pow_right n: βn
#align commute.self_pow Commute.self_powβ: β {M : Type u_1} [inst : Monoid M] (a : M) (n : β), Commute a (a ^ n)Commute.self_powβ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

-- porting note: `simpNF` told me to remove the `simp` attribute
theorem pow_self: β (a : M) (n : β), Commute (a ^ n) apow_self (a: Ma : M: Type ?u.7330M) (n: βn : β: Typeβ) : Commute: {S : Type ?u.7363} β [inst : Mul S] β S β S β PropCommute (a: Ma ^ n: βn) a: Ma :=
(Commute.refl: β {S : Type ?u.7685} [inst : Mul S] (a : S), Commute a aCommute.refl a: Ma).pow_left: β {M : Type ?u.7707} [inst : Monoid M] {a b : M}, Commute a b β β (n : β), Commute (a ^ n) bpow_left n: βn
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`
#align commute.pow_self Commute.pow_self: β {M : Type u_1} [inst : Monoid M] (a : M) (n : β), Commute (a ^ n) aCommute.pow_self

-- porting note: `simpNF` told me to remove the `simp` attribute
@[to_additive: β {M : Type u_1} [inst : AddMonoid M] (a : M) (m n : β), AddCommute (m β’ a) (n β’ a)to_additive]
theorem pow_pow_self: β {M : Type u_1} [inst : Monoid M] (a : M) (m n : β), Commute (a ^ m) (a ^ n)pow_pow_self (a: Ma : M: Type ?u.7757M) (m: βm n: βn : β: Typeβ) : Commute: {S : Type ?u.7792} β [inst : Mul S] β S β S β PropCommute (a: Ma ^ m: βm) (a: Ma ^ n: βn) :=
(Commute.refl: β {S : Type ?u.8356} [inst : Mul S] (a : S), Commute a aCommute.refl a: Ma).pow_pow: β {M : Type ?u.8378} [inst : Monoid M] {a b : M}, Commute a b β β (m n : β), Commute (a ^ m) (b ^ n)pow_pow m: βm n: βn
#align commute.pow_pow_self Commute.pow_pow_selfβ: β {M : Type u_1} [inst : Monoid M] (a : M) (m n : β), Commute (a ^ m) (a ^ n)Commute.pow_pow_selfβ
-- `MulOneClass.toHasMul` vs. `MulOneClass.toMul`

@[to_additive succ_nsmul': β {M : Type u_1} [inst : AddMonoid M] (a : M) (n : β), (n + 1) β’ a = n β’ a + asucc_nsmul']
theorem _root_.pow_succ': β {M : Type u_1} [inst : Monoid M] (a : M) (n : β), a ^ (n + 1) = a ^ n * a_root_.pow_succ' (a: Ma : M: Type ?u.8434M) (n: βn : β: Typeβ) : a: Ma ^ (n: βn + 1: ?m.84751) = a: Ma ^ n: βn * a: Ma :=
(pow_succ: β {M : Type ?u.8963} [inst : Monoid M] (a : M) (n : β), a ^ (n + 1) = a * a ^ npow_succ a: Ma n: βn).trans: β {Ξ± : Sort ?u.8973} {a b c : Ξ±}, a = b β b = c β a = ctrans (self_pow: β {M : Type ?u.8987} [inst : Monoid M] (a : M) (n : β), Commute a (a ^ n)self_pow _: ?m.8988_ _: β_)
#align pow_succ' pow_succ': β {M : Type u_1} [inst : Monoid M] (a : M) (n : β), a ^ (n + 1) = a ^ n * apow_succ'
#align succ_nsmul' succ_nsmul': β {M : Type u_1} [inst : AddMonoid M] (a : M) (n : β), (n + 1) β’ a = n β’ a + asucc_nsmul'

theorem units_inv_right: Commute a βu β Commute a βuβ»ΒΉunits_inv_right : Commute: {S : Type ?u.9071} β [inst : Mul S] β S β S β PropCommute a: Ma u: MΛ£u β Commute: {S : Type ?u.9226} β [inst : Mul S] β S β S β PropCommute a: Ma βu: MΛ£uβ»ΒΉ :=
SemiconjBy.units_inv_right: β {M : Type ?u.9348} [inst : Monoid M] {a : M} {x y : MΛ£}, SemiconjBy a βx βy β SemiconjBy a βxβ»ΒΉ βyβ»ΒΉSemiconjBy.units_inv_right
#align commute.units_inv_right Commute.units_inv_right: β {M : Type u_1} [inst : Monoid M] {a : M} {u : MΛ£}, Commute a βu β Commute a βuβ»ΒΉCommute.units_inv_right

theorem units_inv_right_iff: Commute a βuβ»ΒΉ β Commute a βuunits_inv_right_iff : Commute: {S : Type ?u.9437} β [inst : Mul S] β S β S β PropCommute a: Ma βu: MΛ£uβ»ΒΉ β Commute: {S : Type ?u.9599} β [inst : Mul S] β S β S β PropCommute a: Ma u: MΛ£u :=
SemiconjBy.units_inv_right_iff: β {M : Type ?u.9704} [inst : Monoid M] {a : M} {x y : MΛ£}, SemiconjBy a βxβ»ΒΉ βyβ»ΒΉ β SemiconjBy a βx βySemiconjBy.units_inv_right_iff
#align commute.units_inv_right_iff Commute.units_inv_right_iff: β {M : Type u_1} [inst : Monoid M] {a : M} {u : MΛ£}, Commute a βuβ»ΒΉ β Commute a βuCommute.units_inv_right_iff

theorem units_inv_left: β {M : Type u_1} [inst : Monoid M] {a : M} {u : MΛ£}, Commute (βu) a β Commute (βuβ»ΒΉ) aunits_inv_left : Commute: {S : Type ?u.9844} β [inst : Mul S] β S β S β PropCommute (βu: MΛ£u) a: Ma β Commute: {S : Type ?u.9872} β [inst : Mul S] β S β S β PropCommute (βu: MΛ£uβ»ΒΉ) a: Ma :=
SemiconjBy.units_inv_symm_left: β {M : Type ?u.10123} [inst : Monoid M] {a : MΛ£} {x y : M}, SemiconjBy (βa) x y β SemiconjBy (βaβ»ΒΉ) y xSemiconjBy.units_inv_symm_left
#align commute.units_inv_left Commute.units_inv_left: β {M : Type u_1} [inst : Monoid M] {a : M} {u : MΛ£}, Commute (βu) a β Commute (βuβ»ΒΉ) aCommute.units_inv_left

theorem units_inv_left_iff: Commute (βuβ»ΒΉ) a β Commute (βu) aunits_inv_left_iff : Commute: {S : Type ?u.10212} β [inst : Mul S] β S β S β PropCommute (βu: MΛ£uβ»ΒΉ) a: Ma β Commute: {S : Type ?u.10235} β [inst : Mul S] β S β S β PropCommute (βu: MΛ£u) a: Ma :=
SemiconjBy.units_inv_symm_left_iff: β {M : Type ?u.10481} [inst : Monoid M] {a : MΛ£} {x y : M}, SemiconjBy (βaβ»ΒΉ) y x β SemiconjBy (βa) x ySemiconjBy.units_inv_symm_left_iff
#align commute.units_inv_left_iff Commute.units_inv_left_iff: β {M : Type u_1} [inst : Monoid M] {a : M} {u : MΛ£}, Commute (βuβ»ΒΉ) a β Commute (βu) aCommute.units_inv_left_iff

theorem units_val: Commute uβ uβ β Commute βuβ βuβunits_val : Commute: {S : Type ?u.10621} β [inst : Mul S] β S β S β PropCommute uβ: MΛ£uβ uβ: MΛ£uβ β Commute: {S : Type ?u.10648} β [inst : Mul S] β S β S β PropCommute (uβ: MΛ£uβ : M: Type ?u.10591M) uβ: MΛ£uβ :=
SemiconjBy.units_val: β {M : Type ?u.10896} [inst : Monoid M] {a x y : MΛ£}, SemiconjBy a x y β SemiconjBy βa βx βySemiconjBy.units_val
#align commute.units_coe Commute.units_val: β {M : Type u_1} [inst : Monoid M] {uβ uβ : MΛ£}, Commute uβ uβ β Commute βuβ βuβCommute.units_val

theorem units_of_val: β {M : Type u_1} [inst : Monoid M] {uβ uβ : MΛ£}, Commute βuβ βuβ β Commute uβ uβunits_of_val : Commute: {S : Type ?u.10983} β [inst : Mul S] β S β S β PropCommute (uβ: MΛ£uβ : M: Type ?u.10953M) uβ: MΛ£uβ β Commute: {S : Type ?u.11240} β [inst : Mul S] β S β S β PropCommute uβ: MΛ£uβ uβ: MΛ£uβ :=
SemiconjBy.units_of_val: β {M : Type ?u.11258} [inst : Monoid M] {a x y : MΛ£}, SemiconjBy βa βx βy β SemiconjBy a x ySemiconjBy.units_of_val
#align commute.units_of_coe Commute.units_of_val: β {M : Type u_1} [inst : Monoid M] {uβ uβ : MΛ£}, Commute βuβ βuβ β Commute uβ uβCommute.units_of_val

theorem units_val_iff: β {M : Type u_1} [inst : Monoid M] {uβ uβ : MΛ£}, Commute βuβ βuβ β Commute uβ uβunits_val_iff : Commute: {S : Type ?u.11347} β [inst : Mul S] β S β S β PropCommute (uβ: MΛ£uβ : M: Type ?u.11318M) uβ: MΛ£uβ β Commute: {S : Type ?u.11599} β [inst : Mul S] β S β S β PropCommute uβ: MΛ£uβ uβ: MΛ£uβ :=
SemiconjBy.units_val_iff: β {M : Type ?u.11612} [inst : Monoid M] {a x y : MΛ£}, SemiconjBy βa βx βy β SemiconjBy a x ySemiconjBy.units_val_iff
#align commute.units_coe_iff Commute.units_val_iff: β {M : Type u_1} [inst : Monoid M] {uβ uβ : MΛ£}, Commute βuβ βuβ β Commute uβ uβCommute.units_val_iff

/-- If the product of two commuting elements is a unit, then the left multiplier is a unit. -/
@[to_additive: {M : Type u_1} β [inst : AddMonoid M] β (u : AddUnits M) β (a b : M) β a + b = βu β AddCommute a b β AddUnits Mto_additive "If the sum of two commuting elements is an additive unit, then the left summand is
def _root_.Units.leftOfMul: (u : MΛ£) β (a b : M) β a * b = βu β Commute a b β MΛ£_root_.Units.leftOfMul (u: MΛ£u : M: Type ?u.11709MΛ£) (a: Ma b: Mb : M: Type ?u.11709M) (hu: a * b = βuhu : a: Ma * b: Mb = u: MΛ£u) (hc: Commute a bhc : Commute: {S : Type ?u.12046} β [inst : Mul S] β S β S β PropCommute a: Ma b: Mb) : M: Type ?u.11709MΛ£ where
val := a: Ma
inv := b: Mb * βu: MΛ£uβ»ΒΉ
val_inv := byGoals accomplished! π G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a ba * (b * βuβ»ΒΉ) = 1rw [G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a ba * (b * βuβ»ΒΉ) = 1β mul_assoc: β {G : Type ?u.12230} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a ba * b * βuβ»ΒΉ = 1 G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a ba * (b * βuβ»ΒΉ) = 1hu: a * b = βuhu,G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bβu * βuβ»ΒΉ = 1 G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a ba * (b * βuβ»ΒΉ) = 1u: MΛ£u.mul_inv: β {Ξ± : Type ?u.12289} [inst : Monoid Ξ±] (a : Ξ±Λ£), βa * βaβ»ΒΉ = 1mul_invG: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a b1 = 1]Goals accomplished! π
inv_val := byGoals accomplished! π
G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bb * βuβ»ΒΉ * a = 1have : Commute: {S : Type ?u.12303} β [inst : Mul S] β S β S β PropCommute a: Ma u: MΛ£u := hu: a * b = βuhu βΈ (Commute.refl: β {S : Type ?u.12411} [inst : Mul S] (a : S), Commute a aCommute.refl _: ?m.12412_).mul_right: β {S : Type ?u.12419} [inst : Semigroup S] {a b c : S}, Commute a b β Commute a c β Commute a (b * c)mul_right hc: Commute a bhcG: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bthis: Commute a βub * βuβ»ΒΉ * a = 1
G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bb * βuβ»ΒΉ * a = 1rw [G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bthis: Commute a βub * βuβ»ΒΉ * a = 1β this: Commute a βuthis.units_inv_right: β {M : Type ?u.12476} [inst : Monoid M] {a : M} {u : MΛ£}, Commute a βu β Commute a βuβ»ΒΉunits_inv_right.right_comm: β {S : Type ?u.12486} [inst : Semigroup S] {b c : S}, Commute b c β β (a : S), a * b * c = a * c * bright_comm,G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bthis: Commute a βub * a * βuβ»ΒΉ = 1 G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bthis: Commute a βub * βuβ»ΒΉ * a = 1β hc: Commute a bhc.eq: β {S : Type ?u.12502} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq,G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bthis: Commute a βua * b * βuβ»ΒΉ = 1 G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bthis: Commute a βub * βuβ»ΒΉ * a = 1hu: a * b = βuhu,G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bthis: Commute a βuβu * βuβ»ΒΉ = 1 G: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bthis: Commute a βub * βuβ»ΒΉ * a = 1u: MΛ£u.mul_inv: β {Ξ± : Type ?u.12518} [inst : Monoid Ξ±] (a : Ξ±Λ£), βa * βaβ»ΒΉ = 1mul_invG: Type ?u.11706M: Type ?u.11709instβ: Monoid Maβ, bβ: Muβ, uβ, uβ, u: MΛ£a, b: Mhu: a * b = βuhc: Commute a bthis: Commute a βu1 = 1]Goals accomplished! π
#align units.left_of_mul Units.leftOfMul: {M : Type u_1} β [inst : Monoid M] β (u : MΛ£) β (a b : M) β a * b = βu β Commute a b β MΛ£Units.leftOfMul

/-- If the product of two commuting elements is a unit, then the right multiplier is a unit. -/
@[to_additive: {M : Type u_1} β [inst : AddMonoid M] β (u : AddUnits M) β (a b : M) β a + b = βu β AddCommute a b β AddUnits Mto_additive "If the sum of two commuting elements is an additive unit, then the right summand
def _root_.Units.rightOfMul: {M : Type u_1} β [inst : Monoid M] β (u : MΛ£) β (a b : M) β a * b = βu β Commute a b β MΛ£_root_.Units.rightOfMul (u: MΛ£u : M: Type ?u.12890MΛ£) (a: Ma b: Mb : M: Type ?u.12890M) (hu: a * b = βuhu : a: Ma * b: Mb = u: MΛ£u) (hc: Commute a bhc : Commute: {S : Type ?u.13227} β [inst : Mul S] β S β S β PropCommute a: Ma b: Mb) : M: Type ?u.12890MΛ£ :=
u: MΛ£u.leftOfMul: {M : Type ?u.13256} β [inst : Monoid M] β (u : MΛ£) β (a b : M) β a * b = βu β Commute a b β MΛ£leftOfMul b: Mb a: Ma (hc: Commute a bhc.eq: β {S : Type ?u.13266} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq βΈ hu: a * b = βuhu) hc: Commute a bhc.symm: β {S : Type ?u.13289} [inst : Mul S] {a b : S}, Commute a b β Commute b asymm
#align units.right_of_mul Units.rightOfMul: {M : Type u_1} β [inst : Monoid M] β (u : MΛ£) β (a b : M) β a * b = βu β Commute a b β MΛ£Units.rightOfMul

theorem isUnit_mul_iff: β {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b β (IsUnit (a * b) β IsUnit a β§ IsUnit b)isUnit_mul_iff (h: Commute a bh : Commute: {S : Type ?u.13528} β [inst : Mul S] β S β S β PropCommute a: Ma b: Mb) : IsUnit: {M : Type ?u.13556} β [inst : Monoid M] β M β PropIsUnit (a: Ma * b: Mb) β IsUnit: {M : Type ?u.13618} β [inst : Monoid M] β M β PropIsUnit a: Ma β§ IsUnit: {M : Type ?u.13621} β [inst : Monoid M] β M β PropIsUnit b: Mb :=
β¨fun β¨u: MΛ£u, hu: βu = a * bhuβ© => β¨(u: MΛ£u.leftOfMul: {M : Type ?u.13675} β [inst : Monoid M] β (u : MΛ£) β (a b : M) β a * b = βu β Commute a b β MΛ£leftOfMul a: Ma b: Mb hu: βu = a * bhu.symm: β {Ξ± : Sort ?u.13688} {a b : Ξ±}, a = b β b = asymm h: Commute a bh).isUnit: β {M : Type ?u.13709} [inst : Monoid M] (u : MΛ£), IsUnit βuisUnit, (u: MΛ£u.rightOfMul: {M : Type ?u.13718} β [inst : Monoid M] β (u : MΛ£) β (a b : M) β a * b = βu β Commute a b β MΛ£rightOfMul a: Ma b: Mb hu: βu = a * bhu.symm: β {Ξ± : Sort ?u.13728} {a b : Ξ±}, a = b β b = asymm h: Commute a bh).isUnit: β {M : Type ?u.13736} [inst : Monoid M] (u : MΛ£), IsUnit βuisUnitβ©,
fun H: ?m.13809H => H: ?m.13809H.1: β {a b : Prop}, a β§ b β a1.mul: β {M : Type ?u.13815} [inst : Monoid M] {x y : M}, IsUnit x β IsUnit y β IsUnit (x * y)mul H: ?m.13809H.2: β {a b : Prop}, a β§ b β b2β©
#align commute.is_unit_mul_iff Commute.isUnit_mul_iff: β {M : Type u_1} [inst : Monoid M] {a b : M}, Commute a b β (IsUnit (a * b) β IsUnit a β§ IsUnit b)Commute.isUnit_mul_iff

theorem _root_.isUnit_mul_self_iff: IsUnit (a * a) β IsUnit a_root_.isUnit_mul_self_iff : IsUnit: {M : Type ?u.13958} β [inst : Monoid M] β M β PropIsUnit (a: Ma * a: Ma) β IsUnit: {M : Type ?u.14027} β [inst : Monoid M] β M β PropIsUnit a: Ma :=
(Commute.refl: β {S : Type ?u.14031} [inst : Mul S] (a : S), Commute a aCommute.refl a: Ma).isUnit_mul_iff: β {M : Type ?u.14053} [inst : Monoid M] {a b : M}, Commute a b β (IsUnit (a * b) β IsUnit a β§ IsUnit b)isUnit_mul_iff.trans: β {a b c : Prop}, (a β b) β (b β c) β (a β c)trans (and_self_iff: β (p : Prop), p β§ p β pand_self_iff _: Prop_)
-- porting note: `and_self_iff` now has an implicit argument instead of an explicit one.
#align is_unit_mul_self_iff isUnit_mul_self_iff: β {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit (a * a) β IsUnit aisUnit_mul_self_iff

end Monoid

section DivisionMonoid

variable [DivisionMonoid: Type ?u.16707 β Type ?u.16707DivisionMonoid G: Type ?u.14160G] {a: Ga b: Gb c: Gc d: Gd: G: Type ?u.14146G}

protected theorem inv_inv: Commute a b β Commute aβ»ΒΉ bβ»ΒΉinv_inv : Commute: {S : Type ?u.14175} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb β Commute: {S : Type ?u.14222} β [inst : Mul S] β S β S β PropCommute a: Gaβ»ΒΉ b: Gbβ»ΒΉ :=
SemiconjBy.inv_inv_symm: β {G : Type ?u.14273} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a x y β SemiconjBy aβ»ΒΉ yβ»ΒΉ xβ»ΒΉSemiconjBy.inv_inv_symm
#align commute.inv_inv Commute.inv_inv: β {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b β Commute aβ»ΒΉ bβ»ΒΉCommute.inv_inv

@[to_additive: β {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute (-a) (-b) β AddCommute a bto_additive (attr := simp)]
theorem inv_inv_iff: β {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute aβ»ΒΉ bβ»ΒΉ β Commute a binv_inv_iff : Commute: {S : Type ?u.14339} β [inst : Mul S] β S β S β PropCommute a: Gaβ»ΒΉ b: Gbβ»ΒΉ β Commute: {S : Type ?u.14423} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb :=
SemiconjBy.inv_inv_symm_iff: β {G : Type ?u.14427} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy aβ»ΒΉ xβ»ΒΉ yβ»ΒΉ β SemiconjBy a y xSemiconjBy.inv_inv_symm_iff
#align commute.inv_inv_iff Commute.inv_inv_iff: β {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute aβ»ΒΉ bβ»ΒΉ β Commute a bCommute.inv_inv_iff

@[to_additive: β {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b β -(a + b) = -a + -bto_additive]
protected theorem mul_inv: Commute a b β (a * b)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉmul_inv (hab: Commute a bhab : Commute: {S : Type ?u.14543} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb) : (a: Ga * b: Gb)β»ΒΉ = a: Gaβ»ΒΉ * b: Gbβ»ΒΉ := byGoals accomplished! π G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghab: Commute a b(a * b)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉrw [G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghab: Commute a b(a * b)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉhab: Commute a bhab.eq: β {S : Type ?u.14754} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq,G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghab: Commute a b(b * a)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉ G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghab: Commute a b(a * b)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉmul_inv_rev: β {G : Type ?u.14815} [inst : DivisionMonoid G] (a b : G), (a * b)β»ΒΉ = bβ»ΒΉ * aβ»ΒΉmul_inv_revG: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghab: Commute a baβ»ΒΉ * bβ»ΒΉ = aβ»ΒΉ * bβ»ΒΉ]Goals accomplished! π
#align commute.mul_inv Commute.mul_inv: β {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b β (a * b)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉCommute.mul_inv

@[to_additive: β {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b β -(a + b) = -a + -bto_additive]
protected theorem inv: Commute a b β (a * b)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉinv (hab: Commute a bhab : Commute: {S : Type ?u.14898} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb) : (a: Ga * b: Gb)β»ΒΉ = a: Gaβ»ΒΉ * b: Gbβ»ΒΉ := byGoals accomplished! π G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghab: Commute a b(a * b)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉrw [G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghab: Commute a b(a * b)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉhab: Commute a bhab.eq: β {S : Type ?u.15109} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq,G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghab: Commute a b(b * a)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉ G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghab: Commute a b(a * b)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉmul_inv_rev: β {G : Type ?u.15170} [inst : DivisionMonoid G] (a b : G), (a * b)β»ΒΉ = bβ»ΒΉ * aβ»ΒΉmul_inv_revG: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghab: Commute a baβ»ΒΉ * bβ»ΒΉ = aβ»ΒΉ * bβ»ΒΉ]Goals accomplished! π
#align commute.inv Commute.inv: β {G : Type u_1} [inst : DivisionMonoid G] {a b : G}, Commute a b β (a * b)β»ΒΉ = aβ»ΒΉ * bβ»ΒΉCommute.inv
#align add_commute.neg AddCommute.neg: β {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute a b β -(a + b) = -a + -bAddCommute.neg

@[to_additive: β {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
AddCommute b d β AddCommute (-b) c β a - b + (c - d) = a + c - (b + d)to_additive]
protected theorem div_mul_div_comm: β {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
Commute b d β Commute bβ»ΒΉ c β a / b * (c / d) = a * c / (b * d)div_mul_div_comm (hbd: Commute b dhbd : Commute: {S : Type ?u.15253} β [inst : Mul S] β S β S β PropCommute b: Gb d: Gd) (hbc: Commute bβ»ΒΉ chbc : Commute: {S : Type ?u.15301} β [inst : Mul S] β S β S β PropCommute b: Gbβ»ΒΉ c: Gc) :
a: Ga / b: Gb * (c: Gc / d: Gd) = a: Ga * c: Gc / (b: Gb * d: Gd) := byGoals accomplished! π
G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbd: Commute b dhbc: Commute bβ»ΒΉ ca / b * (c / d) = a * c / (b * d)simp_rw [G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbd: Commute b dhbc: Commute bβ»ΒΉ ca / b * (c / d) = a * c / (b * d)div_eq_mul_inv: β {G : Type ?u.15768} [inst : DivInvMonoid G] (a b : G), a / b = a * bβ»ΒΉdiv_eq_mul_inv,G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbd: Commute b dhbc: Commute bβ»ΒΉ ca * bβ»ΒΉ * (c * dβ»ΒΉ) = a * c * (b * d)β»ΒΉ G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbd: Commute b dhbc: Commute bβ»ΒΉ ca / b * (c / d) = a * c / (b * d)mul_inv_rev: β {G : Type ?u.15867} [inst : DivisionMonoid G] (a b : G), (a * b)β»ΒΉ = bβ»ΒΉ * aβ»ΒΉmul_inv_rev,G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbd: Commute b dhbc: Commute bβ»ΒΉ ca * bβ»ΒΉ * (c * dβ»ΒΉ) = a * c * (dβ»ΒΉ * bβ»ΒΉ) G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbd: Commute b dhbc: Commute bβ»ΒΉ ca / b * (c / d) = a * c / (b * d)hbd: Commute b dhbd.inv_inv: β {G : Type ?u.15920} [inst : DivisionMonoid G] {a b : G}, Commute a b β Commute aβ»ΒΉ bβ»ΒΉinv_inv.symm: β {S : Type ?u.15931} [inst : Mul S] {a b : S}, Commute a b β Commute b asymm.eq: β {S : Type ?u.15969} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq,G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbd: Commute b dhbc: Commute bβ»ΒΉ ca * bβ»ΒΉ * (c * dβ»ΒΉ) = a * c * (bβ»ΒΉ * dβ»ΒΉ) G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbd: Commute b dhbc: Commute bβ»ΒΉ ca / b * (c / d) = a * c / (b * d)hbc: Commute bβ»ΒΉ chbc.mul_mul_mul_comm: β {S : Type ?u.16017} [inst : Semigroup S] {b c : S}, Commute b c β β (a d : S), a * b * (c * d) = a * c * (b * d)mul_mul_mul_commGoals accomplished! π]Goals accomplished! π
#align commute.div_mul_div_comm Commute.div_mul_div_comm: β {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
Commute b d β Commute bβ»ΒΉ c β a / b * (c / d) = a * c / (b * d)Commute.div_mul_div_comm
AddCommute b d β AddCommute (-b) c β a - b + (c - d) = a + c - (b + d)AddCommute.sub_add_sub_comm

@[to_additive: β {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
AddCommute c d β AddCommute b (-c) β a + b - (c + d) = a - c + (b - d)to_additive]
protected theorem mul_div_mul_comm: β {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
Commute c d β Commute b cβ»ΒΉ β a * b / (c * d) = a / c * (b / d)mul_div_mul_comm (hcd: Commute c dhcd : Commute: {S : Type ?u.16160} β [inst : Mul S] β S β S β PropCommute c: Gc d: Gd) (hbc: Commute b cβ»ΒΉhbc : Commute: {S : Type ?u.16208} β [inst : Mul S] β S β S β PropCommute b: Gb c: Gcβ»ΒΉ) :
a: Ga * b: Gb / (c: Gc * d: Gd) = a: Ga / c: Gc * (b: Gb / d: Gd) :=
(hcd: Commute c dhcd.div_mul_div_comm: β {G : Type ?u.16563} [inst : DivisionMonoid G] {a b c d : G},
Commute b d β Commute bβ»ΒΉ c β a / b * (c / d) = a * c / (b * d)div_mul_div_comm hbc: Commute b cβ»ΒΉhbc.symm: β {S : Type ?u.16593} [inst : Mul S] {a b : S}, Commute a b β Commute b asymm).symm: β {Ξ± : Sort ?u.16640} {a b : Ξ±}, a = b β b = asymm
#align commute.mul_div_mul_comm Commute.mul_div_mul_comm: β {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
Commute c d β Commute b cβ»ΒΉ β a * b / (c * d) = a / c * (b / d)Commute.mul_div_mul_comm

@[to_additive: β {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
AddCommute b c β AddCommute (-b) d β AddCommute (-c) d β a - b - (c - d) = a - c - (b - d)to_additive]
protected theorem div_div_div_comm: Commute b c β Commute bβ»ΒΉ d β Commute cβ»ΒΉ d β a / b / (c / d) = a / c / (b / d)div_div_div_comm (hbc: Commute b chbc : Commute: {S : Type ?u.16718} β [inst : Mul S] β S β S β PropCommute b: Gb c: Gc) (hbd: Commute bβ»ΒΉ dhbd : Commute: {S : Type ?u.16766} β [inst : Mul S] β S β S β PropCommute b: Gbβ»ΒΉ d: Gd) (hcd: Commute cβ»ΒΉ dhcd : Commute: {S : Type ?u.16806} β [inst : Mul S] β S β S β PropCommute c: Gcβ»ΒΉ d: Gd) :
a: Ga / b: Gb / (c: Gc / d: Gd) = a: Ga / c: Gc / (b: Gb / d: Gd) := byGoals accomplished! π
G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da / b / (c / d) = a / c / (b / d)simp_rw [G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da / b / (c / d) = a / c / (b / d)div_eq_mul_inv: β {G : Type ?u.17146} [inst : DivInvMonoid G] (a b : G), a / b = a * bβ»ΒΉdiv_eq_mul_inv,G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da * bβ»ΒΉ * (c * dβ»ΒΉ)β»ΒΉ = a * cβ»ΒΉ * (b * dβ»ΒΉ)β»ΒΉ G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da / b / (c / d) = a / c / (b / d)mul_inv_rev: β {G : Type ?u.17320} [inst : DivisionMonoid G] (a b : G), (a * b)β»ΒΉ = bβ»ΒΉ * aβ»ΒΉmul_inv_rev,G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da * bβ»ΒΉ * (dβ»ΒΉβ»ΒΉ * cβ»ΒΉ) = a * cβ»ΒΉ * (dβ»ΒΉβ»ΒΉ * bβ»ΒΉ) G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da / b / (c / d) = a / c / (b / d)inv_inv: β {G : Type ?u.17384} [inst : InvolutiveInv G] (a : G), aβ»ΒΉβ»ΒΉ = ainv_inv,G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da * bβ»ΒΉ * (d * cβ»ΒΉ) = a * cβ»ΒΉ * (d * bβ»ΒΉ) G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da / b / (c / d) = a / c / (b / d)hbd: Commute bβ»ΒΉ dhbd.symm: β {S : Type ?u.17430} [inst : Mul S] {a b : S}, Commute a b β Commute b asymm.eq: β {S : Type ?u.17472} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq,G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da * bβ»ΒΉ * (d * cβ»ΒΉ) = a * cβ»ΒΉ * (bβ»ΒΉ * d) G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da / b / (c / d) = a / c / (b / d)hcd: Commute cβ»ΒΉ dhcd.symm: β {S : Type ?u.17520} [inst : Mul S] {a b : S}, Commute a b β Commute b asymm.eq: β {S : Type ?u.17562} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq,G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da * bβ»ΒΉ * (cβ»ΒΉ * d) = a * cβ»ΒΉ * (bβ»ΒΉ * d)
G: Type u_1instβ: DivisionMonoid Ga, b, c, d: Ghbc: Commute b chbd: Commute bβ»ΒΉ dhcd: Commute cβ»ΒΉ da / b / (c / d) = a / c / (b / d)hbc: Commute b chbc.inv_inv: β {G : Type ?u.17593} [inst : DivisionMonoid G] {a b : G}, Commute a b β Commute aβ»ΒΉ bβ»ΒΉinv_inv.mul_mul_mul_comm: β {S : Type ?u.17604} [inst : Semigroup S] {b c : S}, Commute b c β β (a d : S), a * b * (c * d) = a * c * (b * d)mul_mul_mul_commGoals accomplished! π]Goals accomplished! π
#align commute.div_div_div_comm Commute.div_div_div_comm: β {G : Type u_1} [inst : DivisionMonoid G] {a b c d : G},
Commute b c β Commute bβ»ΒΉ d β Commute cβ»ΒΉ d β a / b / (c / d) = a / c / (b / d)Commute.div_div_div_comm
#align add_commute.sub_sub_sub_comm AddCommute.sub_sub_sub_comm: β {G : Type u_1} [inst : SubtractionMonoid G] {a b c d : G},
AddCommute b c β AddCommute (-b) d β AddCommute (-c) d β a - b - (c - d) = a - c - (b - d)AddCommute.sub_sub_sub_comm

end DivisionMonoid

section Group

variable [Group: Type ?u.18444 β Type ?u.18444Group G: Type ?u.17737G] {a: Ga b: Gb : G: Type ?u.17737G}

theorem inv_right: Commute a b β Commute a bβ»ΒΉinv_right : Commute: {S : Type ?u.17758} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb β Commute: {S : Type ?u.17797} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gbβ»ΒΉ :=
SemiconjBy.inv_right: β {G : Type ?u.17849} [inst : Group G] {a x y : G}, SemiconjBy a x y β SemiconjBy a xβ»ΒΉ yβ»ΒΉSemiconjBy.inv_right
#align commute.inv_right Commute.inv_right: β {G : Type u_1} [inst : Group G] {a b : G}, Commute a b β Commute a bβ»ΒΉCommute.inv_right

theorem inv_right_iff: Commute a bβ»ΒΉ β Commute a binv_right_iff : Commute: {S : Type ?u.17910} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gbβ»ΒΉ β Commute: {S : Type ?u.17987} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb :=
SemiconjBy.inv_right_iff: β {G : Type ?u.17991} [inst : Group G] {a x y : G}, SemiconjBy a xβ»ΒΉ yβ»ΒΉ β SemiconjBy a x ySemiconjBy.inv_right_iff
#align commute.inv_right_iff Commute.inv_right_iff: β {G : Type u_1} [inst : Group G] {a b : G}, Commute a bβ»ΒΉ β Commute a bCommute.inv_right_iff

theorem inv_left: Commute a b β Commute aβ»ΒΉ binv_left : Commute: {S : Type ?u.18105} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb β Commute: {S : Type ?u.18144} β [inst : Mul S] β S β S β PropCommute a: Gaβ»ΒΉ b: Gb :=
SemiconjBy.inv_symm_left: β {G : Type ?u.18196} [inst : Group G] {a x y : G}, SemiconjBy a x y β SemiconjBy aβ»ΒΉ y xSemiconjBy.inv_symm_left
#align commute.inv_left Commute.inv_left: β {G : Type u_1} [inst : Group G] {a b : G}, Commute a b β Commute aβ»ΒΉ bCommute.inv_left

theorem inv_left_iff: β {G : Type u_1} [inst : Group G] {a b : G}, Commute aβ»ΒΉ b β Commute a binv_left_iff : Commute: {S : Type ?u.18257} β [inst : Mul S] β S β S β PropCommute a: Gaβ»ΒΉ b: Gb β Commute: {S : Type ?u.18334} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb :=
SemiconjBy.inv_symm_left_iff: β {G : Type ?u.18338} [inst : Group G] {a x y : G}, SemiconjBy aβ»ΒΉ y x β SemiconjBy a x ySemiconjBy.inv_symm_left_iff
#align commute.inv_left_iff Commute.inv_left_iff: β {G : Type u_1} [inst : Group G] {a b : G}, Commute aβ»ΒΉ b β Commute a bCommute.inv_left_iff

@[to_additive: β {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b β -a + b + a = bto_additive]
protected theorem inv_mul_cancel: β {G : Type u_1} [inst : Group G] {a b : G}, Commute a b β aβ»ΒΉ * b * a = binv_mul_cancel (h: Commute a bh : Commute: {S : Type ?u.18451} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb) : a: Gaβ»ΒΉ * b: Gb * a: Ga = b: Gb := byGoals accomplished! π
G: Type u_1instβ: Group Ga, b: Gh: Commute a baβ»ΒΉ * b * a = brw [G: Type u_1instβ: Group Ga, b: Gh: Commute a baβ»ΒΉ * b * a = bh: Commute a bh.inv_left: β {G : Type ?u.18642} [inst : Group G] {a b : G}, Commute a b β Commute aβ»ΒΉ binv_left.eq: β {S : Type ?u.18659} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq,G: Type u_1instβ: Group Ga, b: Gh: Commute a bb * aβ»ΒΉ * a = b G: Type u_1instβ: Group Ga, b: Gh: Commute a baβ»ΒΉ * b * a = binv_mul_cancel_right: β {G : Type ?u.18714} [inst : Group G] (a b : G), a * bβ»ΒΉ * b = ainv_mul_cancel_rightG: Type u_1instβ: Group Ga, b: Gh: Commute a bb = b]Goals accomplished! π
#align commute.inv_mul_cancel Commute.inv_mul_cancel: β {G : Type u_1} [inst : Group G] {a b : G}, Commute a b β aβ»ΒΉ * b * a = bCommute.inv_mul_cancel

@[to_additive: β {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b β -a + (b + a) = bto_additive]
theorem inv_mul_cancel_assoc: β {G : Type u_1} [inst : Group G] {a b : G}, Commute a b β aβ»ΒΉ * (b * a) = binv_mul_cancel_assoc (h: Commute a bh : Commute: {S : Type ?u.18780} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb) : a: Gaβ»ΒΉ * (b: Gb * a: Ga) = b: Gb := byGoals accomplished! π
G: Type u_1instβ: Group Ga, b: Gh: Commute a baβ»ΒΉ * (b * a) = brw [G: Type u_1instβ: Group Ga, b: Gh: Commute a baβ»ΒΉ * (b * a) = bβ mul_assoc: β {G : Type ?u.18971} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,G: Type u_1instβ: Group Ga, b: Gh: Commute a baβ»ΒΉ * b * a = b G: Type u_1instβ: Group Ga, b: Gh: Commute a baβ»ΒΉ * (b * a) = bh: Commute a bh.inv_mul_cancel: β {G : Type ?u.19063} [inst : Group G] {a b : G}, Commute a b β aβ»ΒΉ * b * a = binv_mul_cancelG: Type u_1instβ: Group Ga, b: Gh: Commute a bb = b]Goals accomplished! π
#align commute.inv_mul_cancel_assoc Commute.inv_mul_cancel_assoc: β {G : Type u_1} [inst : Group G] {a b : G}, Commute a b β aβ»ΒΉ * (b * a) = bCommute.inv_mul_cancel_assoc

@[to_additive: β {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b β a + b + -a = bto_additive]
protected theorem mul_inv_cancel: Commute a b β a * b * aβ»ΒΉ = bmul_inv_cancel (h: Commute a bh : Commute: {S : Type ?u.19132} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb) : a: Ga * b: Gb * a: Gaβ»ΒΉ = b: Gb := byGoals accomplished! π
G: Type u_1instβ: Group Ga, b: Gh: Commute a ba * b * aβ»ΒΉ = brw [G: Type u_1instβ: Group Ga, b: Gh: Commute a ba * b * aβ»ΒΉ = bh: Commute a bh.eq: β {S : Type ?u.19323} [inst : Mul S] {a b : S}, Commute a b β a * b = b * aeq,G: Type u_1instβ: Group Ga, b: Gh: Commute a bb * a * aβ»ΒΉ = b G: Type u_1instβ: Group Ga, b: Gh: Commute a ba * b * aβ»ΒΉ = bmul_inv_cancel_right: β {G : Type ?u.19376} [inst : Group G] (a b : G), a * b * bβ»ΒΉ = amul_inv_cancel_rightG: Type u_1instβ: Group Ga, b: Gh: Commute a bb = b]Goals accomplished! π
#align commute.mul_inv_cancel Commute.mul_inv_cancel: β {G : Type u_1} [inst : Group G] {a b : G}, Commute a b β a * b * aβ»ΒΉ = bCommute.mul_inv_cancel

@[to_additive: β {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b β a + (b + -a) = bto_additive]
theorem mul_inv_cancel_assoc: Commute a b β a * (b * aβ»ΒΉ) = bmul_inv_cancel_assoc (h: Commute a bh : Commute: {S : Type ?u.19450} β [inst : Mul S] β S β S β PropCommute a: Ga b: Gb) : a: Ga * (b: Gb * a: Gaβ»ΒΉ) = b: Gb := byGoals accomplished! π
G: Type u_1instβ: Group Ga, b: Gh: Commute a ba * (b * aβ»ΒΉ) = brw [G: Type u_1instβ: Group Ga, b: Gh: Commute a ba * (b * aβ»ΒΉ) = bβ mul_assoc: β {G : Type ?u.19641} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc,G: Type u_1instβ: Group Ga, b: Gh: Commute a ba * b * aβ»ΒΉ = b G: Type u_1instβ: Group Ga, b: Gh: Commute a ba * (b * aβ»ΒΉ) = bh: Commute a bh.mul_inv_cancel: β {G : Type ?u.19733} [inst : Group G] {a b : G}, Commute a b β a * b * aβ»ΒΉ = bmul_inv_cancelG: Type u_1instβ: Group Ga, b: Gh: Commute a bb = b]Goals accomplished! π
#align commute.mul_inv_cancel_assoc Commute.mul_inv_cancel_assoc: β {G : Type u_1} [inst : Group G] {a b : G}, Commute a b β a * (b * aβ»ΒΉ) = bCommute.mul_inv_cancel_assoc

end Group

end Commute

section CommGroup

variable [CommGroup: Type ?u.20361 β Type ?u.20361CommGroup G: Type ?u.19802G] (a: Ga b: Gb : G: Type ?u.19802G)

@[to_additive: β {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + b + -a = bto_additive (attr := simp)]
theorem mul_inv_cancel_comm: a * b * aβ»ΒΉ = bmul_inv_cancel_comm : a: Ga * b: Gb * a: Gaβ»ΒΉ = b: Gb :=
(Commute.all: β {S : Type ?u.19976} [inst : CommSemigroup S] (a b : S), Commute a bCommute.all a: Ga b: Gb).mul_inv_cancel: β {G : Type ?u.19995} [inst : Group G] {a b : G}, Commute a b β a * b * aβ»ΒΉ = bmul_inv_cancel
#align mul_inv_cancel_comm mul_inv_cancel_comm: β {G : Type u_1} [inst : CommGroup G] (a b : G), a * b * aβ»ΒΉ = bmul_inv_cancel_comm
#align add_neg_cancel_comm add_neg_cancel_comm: β {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + b + -a = badd_neg_cancel_comm

@[to_additive: β {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + (b + -a) = bto_additive (attr := simp)]
theorem mul_inv_cancel_comm_assoc: a * (b * aβ»ΒΉ) = bmul_inv_cancel_comm_assoc : a: Ga * (b: Gb * a: Gaβ»ΒΉ) = b: Gb :=
(Commute.all: β {S : Type ?u.20254} [inst : CommSemigroup S] (a b : S), Commute a bCommute.all a: Ga b: Gb).mul_inv_cancel_assoc: β {G : Type ?u.20273} [inst : Group G] {a b : G}, Commute a b β a * (b * aβ»ΒΉ) = bmul_inv_cancel_assoc
#align mul_inv_cancel_comm_assoc mul_inv_cancel_comm_assoc: β {G : Type u_1} [inst : CommGroup G] (a b : G), a * (b * aβ»ΒΉ) = bmul_inv_cancel_comm_assoc
#align add_neg_cancel_comm_assoc add_neg_cancel_comm_assoc: β {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + (b + -a) = badd_neg_cancel_comm_assoc

@[to_additive: β {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + b + a = bto_additive (attr := simp)]
theorem inv_mul_cancel_comm: aβ»ΒΉ * b * a = binv_mul_cancel_comm : a: Gaβ»ΒΉ * b: Gb * a: Ga = b: Gb :=
(Commute.all: β {S : Type ?u.20532} [inst : CommSemigroup S] (a b : S), Commute a bCommute.all a: Ga b: Gb).inv_mul_cancel: β {G : Type ?u.20551} [inst : Group G] {a b : G}, Commute a b β aβ»ΒΉ * b * a = binv_mul_cancel
#align inv_mul_cancel_comm inv_mul_cancel_comm: β {G : Type u_1} [inst : CommGroup G] (a b : G), aβ»ΒΉ * b * a = binv_mul_cancel_comm
#align neg_add_cancel_comm neg_add_cancel_comm: β {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + b + a = bneg_add_cancel_comm

@[to_additive: β {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + (b + a) = bto_additive (attr := simp)]
theorem inv_mul_cancel_comm_assoc: aβ»ΒΉ * (b * a) = binv_mul_cancel_comm_assoc : a: Gaβ»ΒΉ * (b: Gb * a: Ga) = b: Gb :=
(Commute.all: β {S : Type ?u.20810} [inst : CommSemigroup S] (a b : S), Commute a bCommute.all a: Ga b: Gb).inv_mul_cancel_assoc: β {G : Type ?u.20829} [inst : Group G] {a b : G}, Commute a b β aβ»ΒΉ * (b * a) = binv_mul_cancel_assoc
#align inv_mul_cancel_comm_assoc inv_mul_cancel_comm_assoc: β {G : Type u_1} [inst : CommGroup G] (a b : G), aβ»ΒΉ * (b * a) = binv_mul_cancel_comm_assoc
#align neg_add_cancel_comm_assoc neg_add_cancel_comm_assoc: β {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + (b + a) = bneg_add_cancel_comm_assoc

end CommGroup
```