doc-next-gen

Mathlib.Algebra.Group.Defs

Module docstring

{"# Typeclasses for (semi)groups and monoids

In this file we define typeclasses for algebraic structures with one binary operation. The classes are named (Add)?(Comm)?(Semigroup|Monoid|Group), where Add means that the class uses additive notation and Comm means that the class assumes that the binary operation is commutative.

The file does not contain any lemmas except for

  • axioms of typeclasses restated in the root namespace;
  • lemmas required for instances.

For basic lemmas about these classes see Algebra.Group.Basic.

We register the following instances:

  • Pow M ℕ, for monoids M, and Pow G ℤ for groups G;
  • SMul ℕ M for additive monoids M, and SMul ℤ G for additive groups G.

Notation

  • +, -, *, /, ^ : the usual arithmetic operations; the underlying functions are Add.add, Neg.neg/Sub.sub, Mul.mul, Div.div, and HPow.hPow.

","### Design note on AddMonoid and Monoid

An AddMonoid has a natural ℕ-action, defined by n • a = a + ... + a, that we want to declare as an instance as it makes it possible to use the language of linear algebra. However, there are often other natural ℕ-actions. For instance, for any semiring R, the space of polynomials Polynomial R has a natural R-action defined by multiplication on the coefficients. This means that Polynomial ℕ would have two natural ℕ-actions, which are equal but not defeq. The same goes for linear maps, tensor products, and so on (and even for ℕ itself).

To solve this issue, we embed an ℕ-action in the definition of an AddMonoid (which is by default equal to the naive action a + ... + a, but can be adjusted when needed), and declare a SMul ℕ α instance using this action. See Note [forgetful inheritance] for more explanations on this pattern.

For example, when we define Polynomial R, then we declare the ℕ-action to be by multiplication on each coefficient (using the ℕ-action on R that comes from the fact that R is an AddMonoid). In this way, the two natural SMul ℕ (Polynomial ℕ) instances are defeq.

The tactic to_additive transfers definitions and results from multiplicative monoids to additive monoids. To work, it has to map fields to fields. This means that we should also add corresponding fields to the multiplicative structure Monoid, which could solve defeq problems for powers if needed. These problems do not come up in practice, so most of the time we will not need to adjust the npow field when defining multiplicative objects. ","### Design note on DivInvMonoid/SubNegMonoid and DivisionMonoid/SubtractionMonoid

Those two pairs of made-up classes fulfill slightly different roles.

DivInvMonoid/SubNegMonoid provides the minimum amount of information to define the ℤ action (zpow or zsmul). Further, it provides a div field, matching the forgetful inheritance pattern. This is useful to shorten extension clauses of stronger structures (Group, GroupWithZero, DivisionRing, Field) and for a few structures with a rather weak pseudo-inverse (Matrix).

DivisionMonoid/SubtractionMonoid is targeted at structures with stronger pseudo-inverses. It is an ad hoc collection of axioms that are mainly respected by three things: * Groups * Groups with zero * The pointwise monoids Set α, Finset α, Filter α

It acts as a middle ground for structures with an inversion operator that plays well with multiplication, except for the fact that it might not be a true inverse (a / a ≠ 1 in general). The axioms are pretty arbitrary (many other combinations are equivalent to it), but they are independent: * Without DivisionMonoid.div_eq_mul_inv, you can define / arbitrarily. * Without DivisionMonoid.inv_inv, you can consider WithTop Unit with a⁻¹ = ⊤ for all a. * Without DivisionMonoid.mul_inv_rev, you can consider WithTop α with a⁻¹ = a for all a where α non commutative. * Without DivisionMonoid.inv_eq_of_mul, you can consider any CommMonoid with a⁻¹ = a for all a.

As a consequence, a few natural structures do not fit in this framework. For example, ENNReal respects everything except for the fact that (0 * ∞)⁻¹ = 0⁻¹ = ∞ while ∞⁻¹ * 0⁻¹ = 0 * ∞ = 0. ","We initialize all projections for @[simps] here, so that we don't have to do it in later files.

Note: the lemmas generated for the npow/zpow projections will not apply to x ^ y, since the argument order of these projections doesn't match the argument order of ^. The nsmul/zsmul lemmas will be correct. "}

leftMul definition
: G → G → G
Full source 
/-- `leftMul g` denotes left multiplication by `g` -/
@[to_additive "`leftAdd g` denotes left addition by `g`"]
def leftMul : G → G → G := fun g : G ↦ fun x : G ↦ g * x
Left multiplication by an element in a group
Informal description
The function `leftMul` takes an element `g` of a multiplicative group `G` and returns the function that multiplies any element `x` of `G` by `g` on the left, i.e., the function `x ↦ g * x`.
rightMul definition
: G → G → G
Full source 
/-- `rightMul g` denotes right multiplication by `g` -/
@[to_additive "`rightAdd g` denotes right addition by `g`"]
def rightMul : G → G → G := fun g : G ↦ fun x : G ↦ x * g
Right multiplication by an element in a group
Informal description
For an element \( g \) in a multiplicative group \( G \), the function \( \text{rightMul}(g) \) is defined as the right multiplication by \( g \), i.e., \( \text{rightMul}(g)(x) = x \cdot g \) for any \( x \in G \).
IsLeftCancelMul structure
(G : Type u) [Mul G]
Full source 
/-- A mixin for left cancellative multiplication. -/
class IsLeftCancelMul (G : Type u) [Mul G] : Prop where
  /-- Multiplication is left cancellative. -/
  protected mul_left_cancel : ∀ a b c : G, a * b = a * c → b = c
Left cancellative multiplication
Informal description
A structure asserting that a type `G` with a multiplication operation `*` is left cancellative, meaning that for all elements `a, b, c` in `G`, if `a * b = a * c`, then `b = c`.
IsRightCancelMul structure
(G : Type u) [Mul G]
Full source 
/-- A mixin for right cancellative multiplication. -/
class IsRightCancelMul (G : Type u) [Mul G] : Prop where
  /-- Multiplication is right cancellative. -/
  protected mul_right_cancel : ∀ a b c : G, a * b = c * b → a = c
Right cancellative multiplication
Informal description
A structure asserting that a type `G` with a multiplication operation is right cancellative, meaning that for any elements `a, b, c ∈ G`, if `a * c = b * c`, then `a = b`.
IsCancelMul structure
(G : Type u) [Mul G] : Prop extends IsLeftCancelMul G, IsRightCancelMul G
Full source 
/-- A mixin for cancellative multiplication. -/
class IsCancelMul (G : Type u) [Mul G] : Prop extends IsLeftCancelMul G, IsRightCancelMul G
Cancellative multiplication structure
Informal description
A structure asserting that a type \( G \) with a multiplication operation \( \cdot \) satisfies both left and right cancellation properties. Specifically, for any \( a, b, c \in G \): - Left cancellation: \( a \cdot b = a \cdot c \) implies \( b = c \). - Right cancellation: \( b \cdot a = c \cdot a \) implies \( b = c \).
IsLeftCancelAdd structure
(G : Type u) [Add G]
Full source 
/-- A mixin for left cancellative addition. -/
class IsLeftCancelAdd (G : Type u) [Add G] : Prop where
  /-- Addition is left cancellative. -/
  protected add_left_cancel : ∀ a b c : G, a + b = a + c → b = c
Left cancellative addition
Informal description
A structure asserting that the addition operation on a type $G$ is left cancellative, meaning that for any elements $a, b, c \in G$, if $a + b = a + c$, then $b = c$.
IsRightCancelAdd structure
(G : Type u) [Add G]
Full source 
/-- A mixin for right cancellative addition. -/
class IsRightCancelAdd (G : Type u) [Add G] : Prop where
  /-- Addition is right cancellative. -/
  protected add_right_cancel : ∀ a b c : G, a + b = c + b → a = c
Right cancellative addition
Informal description
A structure asserting that an additive operation on a type $G$ is right cancellative, meaning that for any elements $a, b, c \in G$, if $b + a = c + a$, then $b = c$.
IsCancelAdd structure
(G : Type u) [Add G] : Prop extends IsLeftCancelAdd G, IsRightCancelAdd G
Full source 
/-- A mixin for cancellative addition. -/
class IsCancelAdd (G : Type u) [Add G] : Prop extends IsLeftCancelAdd G, IsRightCancelAdd G
Cancellative Addition Property
Informal description
A structure asserting that an additive operation on a type $G$ is cancellative, meaning that for any elements $a, b, c \in G$, if $a + b = a + c$ or $b + a = c + a$, then $b = c$. This property extends both left and right cancellation properties.
mul_left_cancel theorem
: a * b = a * c → b = c
Full source 
@[to_additive]
theorem mul_left_cancel : a * b = a * c → b = c :=
  IsLeftCancelMul.mul_left_cancel a b c
Left cancellation property for multiplication
Informal description
For any elements $a, b, c$ in a left cancellative multiplicative structure, if $a \cdot b = a \cdot c$, then $b = c$.
mul_left_cancel_iff theorem
: a * b = a * c ↔ b = c
Full source 
@[to_additive]
theorem mul_left_cancel_iff : a * b = a * c ↔ b = c :=
  ⟨mul_left_cancel, congrArg _⟩
Left Cancellation Property for Multiplication: $a \cdot b = a \cdot c \leftrightarrow b = c$
Informal description
For any elements $a, b, c$ in a left cancellative multiplicative structure, the equality $a \cdot b = a \cdot c$ holds if and only if $b = c$.
mul_right_injective theorem
(a : G) : Injective (a * ·)
Full source 
@[to_additive]
theorem mul_right_injective (a : G) : Injective (a * ·) := fun _ _ ↦ mul_left_cancel
Right multiplication by an element is injective in a left cancellative structure
Informal description
For any element $a$ in a left cancellative multiplicative structure $G$, the function $x \mapsto a \cdot x$ is injective.
mul_right_inj theorem
(a : G) {b c : G} : a * b = a * c ↔ b = c
Full source 
@[to_additive (attr := simp)]
theorem mul_right_inj (a : G) {b c : G} : a * b = a * c ↔ b = c :=
  (mul_right_injective a).eq_iff
Left Cancellation Property: $a \cdot b = a \cdot c \leftrightarrow b = c$
Informal description
For any element $a$ in a left cancellative multiplicative structure $G$ and any elements $b, c \in G$, the equality $a \cdot b = a \cdot c$ holds if and only if $b = c$.
mul_ne_mul_right theorem
(a : G) {b c : G} : a * b ≠ a * c ↔ b ≠ c
Full source 
@[to_additive]
theorem mul_ne_mul_right (a : G) {b c : G} : a * b ≠ a * ca * b ≠ a * c ↔ b ≠ c :=
  (mul_right_injective a).ne_iff
Inequality Preservation under Left Multiplication in Left Cancellative Structures
Informal description
For any element $a$ in a left cancellative multiplicative structure $G$ and any elements $b, c \in G$, the inequality $a \cdot b \neq a \cdot c$ holds if and only if $b \neq c$.
mul_right_cancel theorem
: a * b = c * b → a = c
Full source 
@[to_additive]
theorem mul_right_cancel : a * b = c * b → a = c :=
  IsRightCancelMul.mul_right_cancel a b c
Right cancellation law for multiplication
Informal description
For any elements $a, b, c$ in a right cancellative multiplicative structure $G$, if $a \cdot b = c \cdot b$, then $a = c$.
mul_left_injective theorem
(a : G) : Function.Injective (· * a)
Full source 
@[to_additive]
theorem mul_left_injective (a : G) : Function.Injective (· * a) := fun _ _ ↦ mul_right_cancel
Injectivity of Left Multiplication in Right Cancellative Structures
Informal description
For any element $a$ in a right cancellative multiplicative structure $G$, the left multiplication function $x \mapsto x \cdot a$ is injective.
mul_left_inj theorem
(a : G) {b c : G} : b * a = c * a ↔ b = c
Full source 
@[to_additive (attr := simp)]
theorem mul_left_inj (a : G) {b c : G} : b * a = c * a ↔ b = c :=
  (mul_left_injective a).eq_iff
Right Cancellation Law: $b \cdot a = c \cdot a \leftrightarrow b = c$
Informal description
For any element $a$ in a right cancellative multiplicative structure $G$, and for any elements $b, c \in G$, the equality $b \cdot a = c \cdot a$ holds if and only if $b = c$.
mul_ne_mul_left theorem
(a : G) {b c : G} : b * a ≠ c * a ↔ b ≠ c
Full source 
@[to_additive]
theorem mul_ne_mul_left (a : G) {b c : G} : b * a ≠ c * ab * a ≠ c * a ↔ b ≠ c :=
  (mul_left_injective a).ne_iff
Inequality Preservation under Right Multiplication in Cancellative Structures
Informal description
For any element $a$ in a right cancellative multiplicative structure $G$, and for any elements $b, c \in G$, the inequality $b \cdot a \neq c \cdot a$ holds if and only if $b \neq c$.
Semigroup structure
(G : Type u) extends Mul G
Full source 
/-- A semigroup is a type with an associative `(*)`. -/
@[ext]
class Semigroup (G : Type u) extends Mul G where
  /-- Multiplication is associative -/
  protected mul_assoc : ∀ a b c : G, a * b * c = a * (b * c)
Semigroup
Informal description
A semigroup is a type $G$ equipped with a binary operation $*$ that is associative, meaning $(a * b) * c = a * (b * c)$ for all $a, b, c \in G$.
AddSemigroup structure
(G : Type u) extends Add G
Full source 
/-- An additive semigroup is a type with an associative `(+)`. -/
@[ext]
class AddSemigroup (G : Type u) extends Add G where
  /-- Addition is associative -/
  protected add_assoc : ∀ a b c : G, a + b + c = a + (b + c)
Additive Semigroup
Informal description
An additive semigroup is a type $G$ equipped with an associative binary operation $+ : G \times G \to G$, meaning that for all $a, b, c \in G$, the equation $(a + b) + c = a + (b + c)$ holds.
mul_assoc theorem
: ∀ a b c : G, a * b * c = a * (b * c)
Full source 
@[to_additive]
theorem mul_assoc : ∀ a b c : G, a * b * c = a * (b * c) :=
  Semigroup.mul_assoc
Associativity of Multiplication in a Semigroup
Informal description
For any elements $a, b, c$ in a semigroup $G$, the operation $*$ is associative, meaning $(a * b) * c = a * (b * c)$.
AddCommMagma structure
(G : Type u) extends Add G
Full source 
/-- A commutative additive magma is a type with an addition which commutes. -/
@[ext]
class AddCommMagma (G : Type u) extends Add G where
  /-- Addition is commutative in an commutative additive magma. -/
  protected add_comm : ∀ a b : G, a + b = b + a
Additive Commutative Magma
Informal description
An additive commutative magma is a type $G$ equipped with a commutative addition operation $+ : G \to G \to G$, meaning that for all $a, b \in G$, we have $a + b = b + a$.
CommMagma structure
(G : Type u) extends Mul G
Full source 
/-- A commutative multiplicative magma is a type with a multiplication which commutes. -/
@[ext]
class CommMagma (G : Type u) extends Mul G where
  /-- Multiplication is commutative in a commutative multiplicative magma. -/
  protected mul_comm : ∀ a b : G, a * b = b * a
Commutative magma
Informal description
A commutative magma is a type $G$ equipped with a binary operation $*$ that is commutative, i.e., for all $a, b \in G$, $a * b = b * a$.
CommSemigroup structure
(G : Type u) extends Semigroup G, CommMagma G
Full source 
/-- A commutative semigroup is a type with an associative commutative `(*)`. -/
@[ext]
class CommSemigroup (G : Type u) extends Semigroup G, CommMagma G where
Commutative semigroup
Informal description
A commutative semigroup is a type $G$ equipped with an associative and commutative binary operation $* : G \times G \to G$.
AddCommSemigroup structure
(G : Type u) extends AddSemigroup G, AddCommMagma G
Full source 
/-- A commutative additive semigroup is a type with an associative commutative `(+)`. -/
@[ext]
class AddCommSemigroup (G : Type u) extends AddSemigroup G, AddCommMagma G where
Additive Commutative Semigroup
Informal description
An additive commutative semigroup is a type $G$ equipped with an associative and commutative binary operation $+ : G \times G \to G$.
mul_comm theorem
: ∀ a b : G, a * b = b * a
Full source 
@[to_additive]
theorem mul_comm : ∀ a b : G, a * b = b * a := CommMagma.mul_comm
Commutativity of Binary Operation in a Commutative Magma
Informal description
For any two elements $a$ and $b$ in a commutative magma $G$, the binary operation $*$ satisfies $a * b = b * a$.
CommMagma.IsRightCancelMul.toIsLeftCancelMul theorem
(G : Type u) [CommMagma G] [IsRightCancelMul G] : IsLeftCancelMul G
Full source 
/-- Any `CommMagma G` that satisfies `IsRightCancelMul G` also satisfies `IsLeftCancelMul G`. -/
@[to_additive AddCommMagma.IsRightCancelAdd.toIsLeftCancelAdd "Any `AddCommMagma G` that satisfies
`IsRightCancelAdd G` also satisfies `IsLeftCancelAdd G`."]
lemma CommMagma.IsRightCancelMul.toIsLeftCancelMul (G : Type u) [CommMagma G] [IsRightCancelMul G] :
    IsLeftCancelMul G :=
  ⟨fun _ _ _ h => mul_right_cancel <| (mul_comm _ _).trans (h.trans (mul_comm _ _))⟩
Right cancellativity implies left cancellativity in a commutative magma
Informal description
For any commutative magma $G$ with a right cancellative multiplication operation, the multiplication is also left cancellative. That is, if $G$ satisfies $a * c = b * c \implies a = b$ for all $a, b, c \in G$, then it also satisfies $a * b = a * c \implies b = c$ for all $a, b, c \in G$.
CommMagma.IsLeftCancelMul.toIsRightCancelMul theorem
(G : Type u) [CommMagma G] [IsLeftCancelMul G] : IsRightCancelMul G
Full source 
/-- Any `CommMagma G` that satisfies `IsLeftCancelMul G` also satisfies `IsRightCancelMul G`. -/
@[to_additive AddCommMagma.IsLeftCancelAdd.toIsRightCancelAdd "Any `AddCommMagma G` that satisfies
`IsLeftCancelAdd G` also satisfies `IsRightCancelAdd G`."]
lemma CommMagma.IsLeftCancelMul.toIsRightCancelMul (G : Type u) [CommMagma G] [IsLeftCancelMul G] :
    IsRightCancelMul G :=
  ⟨fun _ _ _ h => mul_left_cancel <| (mul_comm _ _).trans (h.trans (mul_comm _ _))⟩
Left cancellativity implies right cancellativity in a commutative magma
Informal description
For any commutative magma $G$ with a left cancellative multiplication operation, the multiplication is also right cancellative. That is, if $G$ satisfies $a \cdot b = a \cdot c \implies b = c$ for all $a, b, c \in G$, then it also satisfies $a \cdot c = b \cdot c \implies a = b$ for all $a, b, c \in G$.
CommMagma.IsLeftCancelMul.toIsCancelMul theorem
(G : Type u) [CommMagma G] [IsLeftCancelMul G] : IsCancelMul G
Full source 
/-- Any `CommMagma G` that satisfies `IsLeftCancelMul G` also satisfies `IsCancelMul G`. -/
@[to_additive AddCommMagma.IsLeftCancelAdd.toIsCancelAdd "Any `AddCommMagma G` that satisfies
`IsLeftCancelAdd G` also satisfies `IsCancelAdd G`."]
lemma CommMagma.IsLeftCancelMul.toIsCancelMul (G : Type u) [CommMagma G] [IsLeftCancelMul G] :
    IsCancelMul G := { CommMagma.IsLeftCancelMul.toIsRightCancelMul G with }
Left cancellativity implies full cancellativity in a commutative magma
Informal description
Let $G$ be a commutative magma with a left cancellative multiplication operation. Then the multiplication is also right cancellative, and hence $G$ satisfies both left and right cancellation properties. That is, for all $a, b, c \in G$: - If $a \cdot b = a \cdot c$, then $b = c$ (left cancellation). - If $b \cdot a = c \cdot a$, then $b = c$ (right cancellation).
CommMagma.IsRightCancelMul.toIsCancelMul theorem
(G : Type u) [CommMagma G] [IsRightCancelMul G] : IsCancelMul G
Full source 
/-- Any `CommMagma G` that satisfies `IsRightCancelMul G` also satisfies `IsCancelMul G`. -/
@[to_additive AddCommMagma.IsRightCancelAdd.toIsCancelAdd "Any `AddCommMagma G` that satisfies
`IsRightCancelAdd G` also satisfies `IsCancelAdd G`."]
lemma CommMagma.IsRightCancelMul.toIsCancelMul (G : Type u) [CommMagma G] [IsRightCancelMul G] :
    IsCancelMul G := { CommMagma.IsRightCancelMul.toIsLeftCancelMul G with }
Right cancellativity implies cancellativity in commutative magmas
Informal description
For any commutative magma $G$ with a right cancellative multiplication operation, the multiplication is also left cancellative, and hence $G$ satisfies both left and right cancellation properties. That is, if for all $a, b, c \in G$ we have $a * c = b * c \implies a = b$, then it also satisfies $a * b = a * c \implies b = c$ and thus forms a cancellative magma.
LeftCancelSemigroup structure
(G : Type u) extends Semigroup G
Full source 
/-- A `LeftCancelSemigroup` is a semigroup such that `a * b = a * c` implies `b = c`. -/
@[ext]
class LeftCancelSemigroup (G : Type u) extends Semigroup G where
  protected mul_left_cancel : ∀ a b c : G, a * b = a * c → b = c
Left Cancellative Semigroup
Informal description
A left cancellative semigroup is a semigroup $(G, *)$ where the operation $*$ satisfies the left cancellation property: for all $a, b, c \in G$, if $a * b = a * c$, then $b = c$.
AddLeftCancelSemigroup structure
(G : Type u) extends AddSemigroup G
Full source 
/-- An `AddLeftCancelSemigroup` is an additive semigroup such that
`a + b = a + c` implies `b = c`. -/
@[ext]
class AddLeftCancelSemigroup (G : Type u) extends AddSemigroup G where
  protected add_left_cancel : ∀ a b c : G, a + b = a + c → b = c
Additive Left-Cancellative Semigroup
Informal description
An additive left-cancellative semigroup is an additive semigroup $(G, +)$ where for any elements $a, b, c \in G$, the equation $a + b = a + c$ implies $b = c$.
LeftCancelSemigroup.toIsLeftCancelMul instance
(G : Type u) [LeftCancelSemigroup G] : IsLeftCancelMul G
Full source 
/-- Any `LeftCancelSemigroup` satisfies `IsLeftCancelMul`. -/
@[to_additive AddLeftCancelSemigroup.toIsLeftCancelAdd "Any `AddLeftCancelSemigroup` satisfies
`IsLeftCancelAdd`."]
instance (priority := 100) LeftCancelSemigroup.toIsLeftCancelMul (G : Type u)
    [LeftCancelSemigroup G] : IsLeftCancelMul G :=
  { mul_left_cancel := LeftCancelSemigroup.mul_left_cancel }
Left Cancellation Property in Left Cancellative Semigroups
Informal description
Every left cancellative semigroup $(G, *)$ satisfies the left cancellation property for multiplication: for all $a, b, c \in G$, if $a * b = a * c$, then $b = c$.
RightCancelSemigroup structure
(G : Type u) extends Semigroup G
Full source 
/-- A `RightCancelSemigroup` is a semigroup such that `a * b = c * b` implies `a = c`. -/
@[ext]
class RightCancelSemigroup (G : Type u) extends Semigroup G where
  protected mul_right_cancel : ∀ a b c : G, a * b = c * b → a = c
Right-Cancellative Semigroup
Informal description
A right-cancellative semigroup is a semigroup $(G, *)$ where for any elements $a, b, c \in G$, the equation $a * b = c * b$ implies $a = c$.
AddRightCancelSemigroup structure
(G : Type u) extends AddSemigroup G
Full source 
/-- An `AddRightCancelSemigroup` is an additive semigroup such that
`a + b = c + b` implies `a = c`. -/
@[ext]
class AddRightCancelSemigroup (G : Type u) extends AddSemigroup G where
  protected add_right_cancel : ∀ a b c : G, a + b = c + b → a = c
Right cancellative additive semigroup
Informal description
An additive semigroup $(G, +)$ is called right cancellative if for all $a, b, c \in G$, the equality $a + b = c + b$ implies $a = c$.
RightCancelSemigroup.toIsRightCancelMul instance
(G : Type u) [RightCancelSemigroup G] : IsRightCancelMul G
Full source 
/-- Any `RightCancelSemigroup` satisfies `IsRightCancelMul`. -/
@[to_additive AddRightCancelSemigroup.toIsRightCancelAdd "Any `AddRightCancelSemigroup` satisfies
`IsRightCancelAdd`."]
instance (priority := 100) RightCancelSemigroup.toIsRightCancelMul (G : Type u)
    [RightCancelSemigroup G] : IsRightCancelMul G :=
  { mul_right_cancel := RightCancelSemigroup.mul_right_cancel }
Right Cancellation Property in Right-Cancellative Semigroups
Informal description
Every right-cancellative semigroup $G$ satisfies the right cancellation property for multiplication, meaning that for any elements $a, b, c \in G$, if $a * c = b * c$, then $a = b$.
MulOneClass structure
(M : Type u) extends One M, Mul M
Full source 
/-- Typeclass for expressing that a type `M` with multiplication and a one satisfies
`1 * a = a` and `a * 1 = a` for all `a : M`. -/
class MulOneClass (M : Type u) extends One M, Mul M where
  /-- One is a left neutral element for multiplication -/
  protected one_mul : ∀ a : M, 1 * a = a
  /-- One is a right neutral element for multiplication -/
  protected mul_one : ∀ a : M, a * 1 = a
Multiplicative structure with identity
Informal description
The structure `MulOneClass M` represents a type `M` equipped with a multiplication operation and a multiplicative identity element `1`, satisfying the axioms `1 * a = a` and `a * 1 = a` for all `a ∈ M`.
AddZeroClass structure
(M : Type u) extends Zero M, Add M
Full source 
/-- Typeclass for expressing that a type `M` with addition and a zero satisfies
`0 + a = a` and `a + 0 = a` for all `a : M`. -/
class AddZeroClass (M : Type u) extends Zero M, Add M where
  /-- Zero is a left neutral element for addition -/
  protected zero_add : ∀ a : M, 0 + a = a
  /-- Zero is a right neutral element for addition -/
  protected add_zero : ∀ a : M, a + 0 = a
Additive Zero Class
Informal description
The structure `AddZeroClass M` represents a type `M` equipped with a zero element `0` and an addition operation `+`, satisfying the additive identity laws: `0 + a = a` and `a + 0 = a` for all `a ∈ M`.
MulOneClass.ext theorem
{M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁.mul = m₂.mul → m₁ = m₂
Full source 
@[to_additive (attr := ext)]
theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁.mul = m₂.mul → m₁ = m₂ := by
  rintro @⟨⟨one₁⟩, ⟨mul₁⟩, one_mul₁, mul_one₁⟩ @⟨⟨one₂⟩, ⟨mul₂⟩, one_mul₂, mul_one₂⟩ ⟨rfl⟩
  -- FIXME (See https://github.com/leanprover/lean4/issues/1711)
  -- congr
  suffices one₁ = one₂ by cases this; rfl
  exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)
Extensionality of Multiplicative Structures with Identity
Informal description
For any two multiplicative structures with identity `m₁` and `m₂` on a type `M`, if their multiplication operations are equal, then `m₁` and `m₂` are equal.
one_mul theorem
: ∀ a : M, 1 * a = a
Full source 
@[to_additive (attr := simp)]
theorem one_mul : ∀ a : M, 1 * a = a :=
  MulOneClass.one_mul
Left identity property in a monoid
Informal description
For any element $a$ in a multiplicative monoid $M$ with identity element $1$, the product of $1$ and $a$ equals $a$, i.e., $1 \cdot a = a$.
mul_one theorem
: ∀ a : M, a * 1 = a
Full source 
@[to_additive (attr := simp)]
theorem mul_one : ∀ a : M, a * 1 = a :=
  MulOneClass.mul_one
Right identity property in a monoid
Informal description
For any element $a$ in a multiplicative monoid $M$ with identity element $1$, the product of $a$ and $1$ equals $a$, i.e., $a \cdot 1 = a$.
npowRec definition
[One M] [Mul M] : ℕ → M → M
Full source 
/-- The fundamental power operation in a monoid. `npowRec n a = a*a*...*a` n times.
Use instead `a ^ n`, which has better definitional behavior. -/
def npowRec [One M] [Mul M] : ℕ → M → M
  | 0, _ => 1
  | n + 1, a => npowRec n a * a
Recursive power operation in a monoid
Informal description
The function `npowRec` takes a natural number `n` and an element `a` of a monoid `M` (with identity element `1` and multiplication operation `*`), and returns the product of `a` multiplied by itself `n` times. Specifically: - For `n = 0`, it returns the identity element `1`. - For `n + 1`, it recursively computes `npowRec n a * a`. This is the fundamental power operation in a monoid, though in practice the notation `a ^ n` is preferred due to better definitional behavior.
nsmulRec definition
[Zero M] [Add M] : ℕ → M → M
Full source 
/-- The fundamental scalar multiplication in an additive monoid. `nsmulRec n a = a+a+...+a` n
times. Use instead `n • a`, which has better definitional behavior. -/
def nsmulRec [Zero M] [Add M] : ℕ → M → M
  | 0, _ => 0
  | n + 1, a => nsmulRec n a + a
Recursive definition of scalar multiplication in an additive monoid
Informal description
The function `nsmulRec` defines scalar multiplication in an additive monoid by repeated addition. Specifically, for a natural number `n` and an element `a` of an additive monoid `M`, `nsmulRec n a` computes the sum `a + a + ... + a` with `n` terms. However, it is recommended to use the notation `n • a` instead, as it has better definitional behavior.
npowRec_add theorem
: npowRec (m + n) a = npowRec m a * npowRec n a
Full source 
@[to_additive] theorem npowRec_add : npowRec (m + n) a = npowRec m a * npowRec n a := by
  obtain _ | n := n; · exact (hn rfl).elim
  induction n with
  | zero => simp only [Nat.zero_add, npowRec, ha]
  | succ n ih => rw [← Nat.add_assoc, npowRec, ih n.succ_ne_zero]; simp only [npowRec, mul_assoc]
Additivity of Recursive Power Operation in a Monoid
Informal description
For any natural numbers $m$ and $n$, and any element $a$ in a monoid, the recursive power operation satisfies $a^{m+n} = a^m * a^n$.
npowRec_succ theorem
: npowRec (n + 1) a = a * npowRec n a
Full source 
@[to_additive] theorem npowRec_succ : npowRec (n + 1) a = a * npowRec n a := by
  rw [Nat.add_comm, npowRec_add 1 n hn a ha, npowRec, npowRec, ha]
Recursive power operation satisfies $a^{n+1} = a \cdot a^n$
Informal description
For any natural number $n$ and any element $a$ in a monoid, the recursive power operation satisfies $a^{n+1} = a \cdot a^n$.
npowBinRec definition
{M : Type*} [One M] [Mul M] (k : ℕ) : M → M
Full source 
/-- Exponentiation by repeated squaring. -/
@[to_additive "Scalar multiplication by repeated self-addition,
the additive version of exponentiation by repeated squaring."]
def npowBinRec {M : Type*} [One M] [Mul M] (k : ℕ) : M → M :=
  npowBinRec.go k 1
where
  /-- Auxiliary tail-recursive implementation for `npowBinRec`. -/
  @[to_additive nsmulBinRec.go "Auxiliary tail-recursive implementation for `nsmulBinRec`."]
  go (k : ℕ) : M → M → M :=
    k.binaryRec (fun y _ ↦ y) fun bn _n fn y x ↦ fn (cond bn (y * x) y) (x * x)
Binary exponentiation in a monoid
Informal description
The function `npowBinRec` computes the $k$-th power of an element $x$ in a multiplicative monoid $M$ (with identity element $1$ and multiplication operation) using exponentiation by repeated squaring. The computation is performed via a tail-recursive auxiliary function that processes the binary representation of $k$ to efficiently compute $x^k$.
npowRec' definition
{M : Type*} [One M] [Mul M] : ℕ → M → M
Full source 
/--
A variant of `npowRec` which is a semigroup homomorphisms from `ℕ₊` to `M`.
-/
def npowRec' {M : Type*} [One M] [Mul M] : ℕ → M → M
  | 0, _ => 1
  | 1, m => m
  | k + 2, m => npowRec' (k + 1) m * m
Recursive definition of powers in a monoid
Informal description
The function `npowRec'` defines the $n$-th power of an element in a multiplicative monoid by recursion on $n$. Specifically: - $0$-th power of any element is $1$ (the multiplicative identity) - $1$-st power of an element $m$ is $m$ itself - For $k+2$, the power is defined recursively as $(k+1)$-th power multiplied by $m$ This gives a semigroup homomorphism from the additive semigroup of positive natural numbers to the multiplicative semigroup $M$.
nsmulRec' definition
{M : Type*} [Zero M] [Add M] : ℕ → M → M
Full source 
/--
A variant of `nsmulRec` which is a semigroup homomorphisms from `ℕ₊` to `M`.
-/
def nsmulRec' {M : Type*} [Zero M] [Add M] : ℕ → M → M
  | 0, _ => 0
  | 1, m => m
  | k + 2, m => nsmulRec' (k + 1) m + m
Recursive definition of natural number scalar multiplication in an additive monoid
Informal description
The function `nsmulRec'` defines scalar multiplication of a natural number `n` with an element `m` of an additive monoid `M` (with zero and addition) by recursion. Specifically: - When `n = 0`, it returns the zero element of `M`. - When `n = 1`, it returns `m` itself. - For `n ≥ 2`, it recursively computes `(n-1) • m` and adds `m` to the result. This function serves as a semigroup homomorphism from the additive semigroup of positive natural numbers to `M`.
npowRec'_succ theorem
{M : Type*} [Mul M] [One M] {k : ℕ} (_ : k ≠ 0) (m : M) : npowRec' (k + 1) m = npowRec' k m * m
Full source 
@[to_additive]
theorem npowRec'_succ {M : Type*} [Mul M] [One M] {k : ℕ} (_ : k ≠ 0) (m : M) :
    npowRec' (k + 1) m = npowRec' k m * m :=
  match k with
  | _ + 1 => rfl
Recursive Power Definition for Successor Case in Monoids
Informal description
For any multiplicative monoid $M$ with identity element $1$ and multiplication operation, and for any nonzero natural number $k$ and element $m \in M$, the $(k+1)$-th power of $m$ defined recursively equals the $k$-th power of $m$ multiplied by $m$, i.e., $$ \text{npowRec'}(k+1, m) = \text{npowRec'}(k, m) \cdot m. $$
npowRec'_two_mul theorem
{M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) : npowRec' (2 * k) m = npowRec' k (m * m)
Full source 
@[to_additive]
theorem npowRec'_two_mul {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
    npowRec' (2 * k) m = npowRec' k (m * m) := by
  induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 0 => rfl
    | 1 => simp [npowRec']
    | k + 2 => simp [npowRec', ← mul_assoc, Nat.mul_add, ← ih]
Recursive Power Identity: $m^{2k} = (m^2)^k$ in Semigroups
Informal description
For any semigroup $M$ with identity element $1$, any natural number $k$, and any element $m \in M$, the $(2k)$-th power of $m$ defined recursively equals the $k$-th power of $m^2$, i.e., $$ m^{2k} = (m^2)^k $$ where powers are defined via the recursive function $\text{npowRec'}$.
npowRec'_mul_comm theorem
{M : Type*} [Semigroup M] [One M] {k : ℕ} (k0 : k ≠ 0) (m : M) : m * npowRec' k m = npowRec' k m * m
Full source 
@[to_additive]
theorem npowRec'_mul_comm {M : Type*} [Semigroup M] [One M] {k : ℕ} (k0 : k ≠ 0) (m : M) :
    m * npowRec' k m = npowRec' k m * m := by
  induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 1 => simp [npowRec', mul_assoc]
    | k + 2 => simp [npowRec', ← mul_assoc, ih]
Commutativity of Element with its Power in Semigroups
Informal description
For any semigroup $M$ with identity element $1$, any nonzero natural number $k$, and any element $m \in M$, the element $m$ commutes with its $k$-th power, i.e., $$ m \cdot m^k = m^k \cdot m $$ where $m^k$ is defined recursively as $\text{npowRec'}(k, m)$.
npowRec_eq theorem
{M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) : npowRec (k + 1) m = 1 * npowRec' (k + 1) m
Full source 
@[to_additive]
theorem npowRec_eq {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) :
    npowRec (k + 1) m = 1 * npowRec' (k + 1) m := by
  induction k using Nat.strongRecOn with
  | ind k' ih =>
    match k' with
    | 0 => rfl
    | k + 1 =>
      rw [npowRec, npowRec'_succ k.succ_ne_zero, ← mul_assoc]
      congr
      simp [ih]
Equivalence of Recursive Power Definitions in Semigroups with Identity
Informal description
For any semigroup $M$ with an identity element $1$, any natural number $k$, and any element $m \in M$, the $(k+1)$-th power of $m$ defined recursively via `npowRec` equals the product of the identity element $1$ with the $(k+1)$-th power of $m$ defined via `npowRec'`. That is, $$ \text{npowRec}(k+1, m) = 1 \cdot \text{npowRec'}(k+1, m). $$
npowBinRec.go_spec theorem
{M : Type*} [Semigroup M] [One M] (k : ℕ) (m n : M) : npowBinRec.go (k + 1) m n = m * npowRec' (k + 1) n
Full source 
@[to_additive]
theorem npowBinRec.go_spec {M : Type*} [Semigroup M] [One M] (k : ℕ) (m n : M) :
    npowBinRec.go (k + 1) m n = m * npowRec' (k + 1) n := by
  unfold go
  generalize hk : k + 1 = k'
  replace hk : k' ≠ 0 := by omega
  induction k' using Nat.binaryRecFromOne generalizing n m with
  | z₀ => simp at hk
  | z₁ => simp [npowRec']
  | f b k' k'0 ih =>
    rw [Nat.binaryRec_eq _ _ (Or.inl rfl), ih _ _ k'0]
    cases b <;> simp only [Nat.bit, cond_false, cond_true, ← Nat.two_mul, npowRec'_two_mul]
    rw [npowRec'_succ (by omega), npowRec'_two_mul, ← npowRec'_two_mul,
      ← npowRec'_mul_comm (by omega), mul_assoc]
Binary Exponentiation Recursion Step: $\text{npowBinRec.go}\,(k+1)\,m\,n = m \cdot n^{k+1}$
Informal description
For any semigroup $M$ with an identity element $1$, any natural number $k$, and any elements $m, n \in M$, the binary exponentiation function `npowBinRec.go` satisfies: $$ \text{npowBinRec.go}\,(k+1)\,m\,n = m \cdot n^{k+1} $$ where $n^{k+1}$ is defined recursively via $\text{npowRec'}$.
npowRecAuto abbrev
{M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) : M
Full source 
/--
An abbreviation for `npowRec` with an additional typeclass assumption on associativity
so that we can use `@[csimp]` to replace it with an implementation by repeated squaring
in compiled code.
-/
@[to_additive
"An abbreviation for `nsmulRec` with an additional typeclass assumptions on associativity
so that we can use `@[csimp]` to replace it with an implementation by repeated doubling in compiled
code as an automatic parameter."]
abbrev npowRecAuto {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) : M :=
  npowRec k m
Automatic power operation in a semigroup with identity
Informal description
Given a semigroup $M$ with a multiplicative identity element $1$, the function `npowRecAuto` takes a natural number $k$ and an element $m \in M$, and returns the product of $m$ multiplied by itself $k$ times. This is an automatically generated implementation of the power operation that ensures associativity.
npowBinRecAuto abbrev
{M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) : M
Full source 
/--
An abbreviation for `npowBinRec` with an additional typeclass assumption on associativity
so that we can use it in `@[csimp]` for more performant code generation.
-/
@[to_additive
"An abbreviation for `nsmulBinRec` with an additional typeclass assumption on associativity
so that we can use it in `@[csimp]` for more performant code generation
as an automatic parameter."]
abbrev npowBinRecAuto {M : Type*} [Semigroup M] [One M] (k : ℕ) (m : M) : M :=
  npowBinRec k m
Binary Exponentiation in a Semigroup with Identity
Informal description
Given a semigroup $M$ with a multiplicative identity element $1$, the function `npowBinRecAuto` computes the $k$-th power of an element $m \in M$ using binary exponentiation (exponentiation by squaring). This provides an efficient implementation of the power operation that maintains associativity.
npowRec_eq_npowBinRec theorem
: @npowRecAuto = @npowBinRecAuto
Full source 
@[to_additive (attr := csimp)]
theorem npowRec_eq_npowBinRec : @npowRecAuto = @npowBinRecAuto := by
  funext M _ _ k m
  rw [npowBinRecAuto, npowRecAuto, npowBinRec]
  match k with
  | 0 => rw [npowRec, npowBinRec.go, Nat.binaryRec_zero]
  | k + 1 => rw [npowBinRec.go_spec, npowRec_eq]
Equality of Recursive and Binary Exponentiation Operations in Semigroups with Identity
Informal description
The recursive power operation `npowRecAuto` in a semigroup with identity is equal to the binary exponentiation operation `npowBinRecAuto`.
AddMonoid structure
(M : Type u) extends AddSemigroup M, AddZeroClass M
Full source 
/-- An `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`. -/
class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where
  /-- Multiplication by a natural number.
  Set this to `nsmulRec` unless `Module` diamonds are possible. -/
  protected nsmul : ℕ → M → M
  /-- Multiplication by `(0 : ℕ)` gives `0`. -/
  protected nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
  /-- Multiplication by `(n + 1 : ℕ)` behaves as expected. -/
  protected nsmul_succ : ∀ (n : ℕ) (x), nsmul (n + 1) x = nsmul n x + x := by intros; rfl
Additive Monoid
Informal description
An additive monoid is an additive semigroup equipped with a zero element `0` that serves as an additive identity, satisfying `0 + a = a + 0 = a` for all elements `a` in the monoid.
Monoid structure
(M : Type u) extends Semigroup M, MulOneClass M
Full source 
/-- A `Monoid` is a `Semigroup` with an element `1` such that `1 * a = a * 1 = a`. -/
@[to_additive]
class Monoid (M : Type u) extends Semigroup M, MulOneClass M where
  /-- Raising to the power of a natural number. -/
  protected npow : ℕ → M → M := npowRecAuto
  /-- Raising to the power `(0 : ℕ)` gives `1`. -/
  protected npow_zero : ∀ x, npow 0 x = 1 := by intros; rfl
  /-- Raising to the power `(n + 1 : ℕ)` behaves as expected. -/
  protected npow_succ : ∀ (n : ℕ) (x), npow (n + 1) x = npow n x * x := by intros; rfl
Monoid
Informal description
A monoid is a semigroup equipped with a multiplicative identity element $1$ such that $1 \cdot a = a \cdot 1 = a$ for all elements $a$ in the monoid.
Monoid.toNatPow instance
{M : Type*} [Monoid M] : Pow M ℕ
Full source 
@[default_instance high] instance Monoid.toNatPow {M : Type*} [Monoid M] : Pow M ℕ :=
  ⟨fun x n ↦ Monoid.npow n x⟩
Natural Number Power Operation on Monoids
Informal description
For any monoid $M$, there is a natural power operation $M \times \mathbb{N} \to M$ defined by repeated multiplication, where $x^n = x \cdot \cdots \cdot x$ ($n$ times).
AddMonoid.toNatSMul instance
{M : Type*} [AddMonoid M] : SMul ℕ M
Full source 
instance AddMonoid.toNatSMul {M : Type*} [AddMonoid M] : SMul ℕ M :=
  ⟨AddMonoid.nsmul⟩
Natural Number Scalar Multiplication on Additive Monoids
Informal description
For any additive monoid $M$, there is a natural scalar multiplication operation $\mathbb{N} \times M \to M$ defined by repeated addition, where $n \cdot a = a + \cdots + a$ ($n$ times).
npow_eq_pow theorem
(n : ℕ) (x : M) : Monoid.npow n x = x ^ n
Full source 
@[to_additive (attr := simp) nsmul_eq_smul]
theorem npow_eq_pow (n : ℕ) (x : M) : Monoid.npow n x = x ^ n :=
  rfl
Monoid Power Operation Equals Exponentiation
Informal description
For any monoid $M$, natural number $n$, and element $x \in M$, the $n$-th power operation defined by the monoid structure equals the $n$-th power of $x$ (written as $x^n$), i.e., $\text{Monoid.npow}\,n\,x = x^n$.
left_inv_eq_right_inv theorem
(hba : b * a = 1) (hac : a * c = 1) : b = c
Full source 
@[to_additive] lemma left_inv_eq_right_inv (hba : b * a = 1) (hac : a * c = 1) : b = c := by
  rw [← one_mul c, ← hba, mul_assoc, hac, mul_one b]
Left and Right Inverses Coincide in a Monoid
Informal description
For any elements $a, b, c$ in a monoid, if $b * a = 1$ and $a * c = 1$, then $b = c$.
pow_zero theorem
(a : M) : a ^ 0 = 1
Full source 
@[to_additive zero_nsmul, simp]
theorem pow_zero (a : M) : a ^ 0 = 1 :=
  Monoid.npow_zero _
Zeroth Power Identity in Monoids: $a^0 = 1$
Informal description
For any element $a$ in a monoid $M$, the zeroth power of $a$ equals the multiplicative identity, i.e., $a^0 = 1$.
pow_succ theorem
(a : M) (n : ℕ) : a ^ (n + 1) = a ^ n * a
Full source 
@[to_additive succ_nsmul]
theorem pow_succ (a : M) (n : ℕ) : a ^ (n + 1) = a ^ n * a :=
  Monoid.npow_succ n a
Recursive Power Formula in Monoids: $a^{n+1} = a^n \cdot a$
Informal description
For any element $a$ in a monoid $M$ and any natural number $n$, the $(n+1)$-th power of $a$ equals the $n$-th power of $a$ multiplied by $a$, i.e., $a^{n+1} = a^n \cdot a$.
pow_one theorem
(a : M) : a ^ 1 = a
Full source 
@[to_additive (attr := simp) one_nsmul]
lemma pow_one (a : M) : a ^ 1 = a := by rw [pow_succ, pow_zero, one_mul]
First Power Identity in Monoids: $a^1 = a$
Informal description
For any element $a$ in a monoid $M$, the first power of $a$ equals $a$ itself, i.e., $a^1 = a$.
pow_succ' theorem
(a : M) : ∀ n, a ^ (n + 1) = a * a ^ n
Full source 
@[to_additive succ_nsmul'] lemma pow_succ' (a : M) : ∀ n, a ^ (n + 1) = a * a ^ n
  | 0 => by simp
  | n + 1 => by rw [pow_succ _ n, pow_succ, pow_succ', mul_assoc]
Recursive Power Formula (Alternative Form): $a^{n+1} = a \cdot a^n$
Informal description
For any element $a$ in a monoid $M$ and any natural number $n$, the $(n+1)$-th power of $a$ equals $a$ multiplied by the $n$-th power of $a$, i.e., $a^{n+1} = a \cdot a^n$.
mul_pow_mul theorem
(a b : M) (n : ℕ) : (a * b) ^ n * a = a * (b * a) ^ n
Full source 
@[to_additive] lemma mul_pow_mul (a b : M) (n : ℕ) :
    (a * b) ^ n * a = a * (b * a) ^ n := by
  induction n with
  | zero => simp
  | succ n ih => simp [pow_succ', ← ih, Nat.mul_add, mul_assoc]
Power of Product Identity: $(ab)^n a = a (ba)^n$
Informal description
For any elements $a, b$ in a monoid $M$ and any natural number $n$, the product of $(a \cdot b)^n$ and $a$ equals the product of $a$ and $(b \cdot a)^n$, i.e., $(a \cdot b)^n \cdot a = a \cdot (b \cdot a)^n$.
pow_mul_comm' theorem
(a : M) (n : ℕ) : a ^ n * a = a * a ^ n
Full source 
@[to_additive]
lemma pow_mul_comm' (a : M) (n : ℕ) : a ^ n * a = a * a ^ n := by rw [← pow_succ, pow_succ']
Commutativity of Powers with Base Element: $a^n \cdot a = a \cdot a^n$
Informal description
For any element $a$ in a monoid $M$ and any natural number $n$, the product of $a^n$ and $a$ equals the product of $a$ and $a^n$, i.e., $a^n \cdot a = a \cdot a^n$.
pow_two theorem
(a : M) : a ^ 2 = a * a
Full source 
/-- Note that most of the lemmas about powers of two refer to it as `sq`. -/
@[to_additive two_nsmul] lemma pow_two (a : M) : a ^ 2 = a * a := by rw [pow_succ, pow_one]
Square of an Element in a Monoid: $a^2 = a \cdot a$
Informal description
For any element $a$ in a monoid $M$, the second power of $a$ equals $a$ multiplied by itself, i.e., $a^2 = a \cdot a$.
pow_three' theorem
(a : M) : a ^ 3 = a * a * a
Full source 
@[to_additive three'_nsmul]
lemma pow_three' (a : M) : a ^ 3 = a * a * a := by rw [pow_succ, pow_two]
Cube of an Element in a Monoid: $a^3 = a \cdot a \cdot a$
Informal description
For any element $a$ in a monoid $M$, the third power of $a$ equals $a$ multiplied by itself three times, i.e., $a^3 = a \cdot a \cdot a$.
pow_three theorem
(a : M) : a ^ 3 = a * (a * a)
Full source 
@[to_additive three_nsmul]
lemma pow_three (a : M) : a ^ 3 = a * (a * a) := by rw [pow_succ', pow_two]
Cube of an Element in a Monoid: $a^3 = a \cdot (a \cdot a)$
Informal description
For any element $a$ in a monoid $M$, the third power of $a$ equals $a$ multiplied by the square of $a$, i.e., $a^3 = a \cdot (a \cdot a)$.
one_pow theorem
: ∀ n, (1 : M) ^ n = 1
Full source 
@[to_additive nsmul_zero, simp] lemma one_pow : ∀ n, (1 : M) ^ n = 1
  | 0 => pow_zero _
  | n + 1 => by rw [pow_succ, one_pow, one_mul]
Identity Power Law: $1^n = 1$ in Monoids
Informal description
For any natural number $n$, the $n$-th power of the multiplicative identity $1$ in a monoid $M$ equals $1$, i.e., $1^n = 1$.
pow_add theorem
(a : M) (m : ℕ) : ∀ n, a ^ (m + n) = a ^ m * a ^ n
Full source 
@[to_additive add_nsmul]
lemma pow_add (a : M) (m : ℕ) : ∀ n, a ^ (m + n) = a ^ m * a ^ n
  | 0 => by rw [Nat.add_zero, pow_zero, mul_one]
  | n + 1 => by rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]
Power Addition Law in Monoids: $a^{m+n} = a^m \cdot a^n$
Informal description
For any element $a$ in a monoid $M$ and any natural numbers $m$ and $n$, the power of $a$ raised to $m + n$ equals the product of $a^m$ and $a^n$, i.e., $a^{m + n} = a^m \cdot a^n$.
pow_mul_comm theorem
(a : M) (m n : ℕ) : a ^ m * a ^ n = a ^ n * a ^ m
Full source 
@[to_additive] lemma pow_mul_comm (a : M) (m n : ℕ) : a ^ m * a ^ n = a ^ n * a ^ m := by
  rw [← pow_add, ← pow_add, Nat.add_comm]
Commutativity of Powers in Monoids: $a^m \cdot a^n = a^n \cdot a^m$
Informal description
For any element $a$ in a monoid $M$ and any natural numbers $m$ and $n$, the product of $a^m$ and $a^n$ is equal to the product of $a^n$ and $a^m$, i.e., $a^m \cdot a^n = a^n \cdot a^m$.
pow_mul theorem
(a : M) (m : ℕ) : ∀ n, a ^ (m * n) = (a ^ m) ^ n
Full source 
@[to_additive mul_nsmul] lemma pow_mul (a : M) (m : ℕ) : ∀ n, a ^ (m * n) = (a ^ m) ^ n
  | 0 => by rw [Nat.mul_zero, pow_zero, pow_zero]
  | n + 1 => by rw [Nat.mul_succ, pow_add, pow_succ, pow_mul]
Power Multiplication Law in Monoids: $a^{m \cdot n} = (a^m)^n$
Informal description
For any element $a$ in a monoid $M$ and any natural numbers $m$ and $n$, the power of $a$ raised to $m \cdot n$ equals the $n$-th power of $a^m$, i.e., $a^{m \cdot n} = (a^m)^n$.
pow_mul' theorem
(a : M) (m n : ℕ) : a ^ (m * n) = (a ^ n) ^ m
Full source 
@[to_additive mul_nsmul']
lemma pow_mul' (a : M) (m n : ℕ) : a ^ (m * n) = (a ^ n) ^ m := by rw [Nat.mul_comm, pow_mul]
Power Multiplication Law (variant): $a^{m \cdot n} = (a^n)^m$ in Monoids
Informal description
For any element $a$ in a monoid $M$ and any natural numbers $m$ and $n$, the power of $a$ raised to $m \cdot n$ equals the $m$-th power of $a^n$, i.e., $a^{m \cdot n} = (a^n)^m$.
pow_right_comm theorem
(a : M) (m n : ℕ) : (a ^ m) ^ n = (a ^ n) ^ m
Full source 
@[to_additive nsmul_left_comm]
lemma pow_right_comm (a : M) (m n : ℕ) : (a ^ m) ^ n = (a ^ n) ^ m := by
  rw [← pow_mul, Nat.mul_comm, pow_mul]
Power Commutation Law in Monoids: $(a^m)^n = (a^n)^m$
Informal description
For any element $a$ in a monoid $M$ and any natural numbers $m$ and $n$, the $n$-th power of $a^m$ equals the $m$-th power of $a^n$, i.e., $(a^m)^n = (a^n)^m$.
AddCommMonoid structure
(M : Type u) extends AddMonoid M, AddCommSemigroup M
Full source 
/-- An additive commutative monoid is an additive monoid with commutative `(+)`. -/
class AddCommMonoid (M : Type u) extends AddMonoid M, AddCommSemigroup M
Additive Commutative Monoid
Informal description
An additive commutative monoid is an additive monoid where the binary operation is commutative. That is, for any elements $x, y$ in the monoid $M$, we have $x + y = y + x$.
CommMonoid structure
(M : Type u) extends Monoid M, CommSemigroup M
Full source 
/-- A commutative monoid is a monoid with commutative `(*)`. -/
@[to_additive]
class CommMonoid (M : Type u) extends Monoid M, CommSemigroup M
Commutative Monoid
Informal description
A commutative monoid is a monoid $(M, \cdot, 1)$ where the binary operation $\cdot$ is commutative, i.e., $a \cdot b = b \cdot a$ for all $a, b \in M$.
AddLeftCancelMonoid structure
(M : Type u) extends AddMonoid M, AddLeftCancelSemigroup M
Full source 
/-- An additive monoid in which addition is left-cancellative.
Main examples are `ℕ` and groups. This is the right typeclass for many sum lemmas, as having a zero
is useful to define the sum over the empty set, so `AddLeftCancelSemigroup` is not enough. -/
class AddLeftCancelMonoid (M : Type u) extends AddMonoid M, AddLeftCancelSemigroup M
Left-Cancellative Additive Monoid
Informal description
An additive monoid $M$ where addition is left-cancellative, meaning that for any elements $a, b, c \in M$, if $a + b = a + c$, then $b = c$. This structure extends both the additive monoid structure and the left-cancellative additive semigroup structure.
LeftCancelMonoid structure
(M : Type u) extends Monoid M, LeftCancelSemigroup M
Full source 
/-- A monoid in which multiplication is left-cancellative. -/
@[to_additive]
class LeftCancelMonoid (M : Type u) extends Monoid M, LeftCancelSemigroup M
Left-cancellative monoid
Informal description
A left-cancellative monoid is a monoid in which the multiplication operation satisfies the left cancellation property: for any elements $a, b, c \in M$, if $a \cdot b = a \cdot c$, then $b = c$.
AddRightCancelMonoid structure
(M : Type u) extends AddMonoid M, AddRightCancelSemigroup M
Full source 
/-- An additive monoid in which addition is right-cancellative.
Main examples are `ℕ` and groups. This is the right typeclass for many sum lemmas, as having a zero
is useful to define the sum over the empty set, so `AddRightCancelSemigroup` is not enough. -/
class AddRightCancelMonoid (M : Type u) extends AddMonoid M, AddRightCancelSemigroup M
Right-cancellative additive monoid
Informal description
An additive monoid \( M \) where addition is right-cancellative, meaning that for any elements \( a, b, c \in M \), if \( b + a = c + a \), then \( b = c \). This structure extends both the additive monoid structure and the right-cancellative additive semigroup structure.
RightCancelMonoid structure
(M : Type u) extends Monoid M, RightCancelSemigroup M
Full source 
/-- A monoid in which multiplication is right-cancellative. -/
@[to_additive]
class RightCancelMonoid (M : Type u) extends Monoid M, RightCancelSemigroup M
Right-cancellative monoid
Informal description
A right-cancellative monoid is a monoid in which the multiplication operation satisfies the right cancellation property: for any elements $a, b, c \in M$, if $b \cdot a = c \cdot a$, then $b = c$.
AddCancelMonoid structure
(M : Type u) extends AddLeftCancelMonoid M, AddRightCancelMonoid M
Full source 
/-- An additive monoid in which addition is cancellative on both sides.
Main examples are `ℕ` and groups. This is the right typeclass for many sum lemmas, as having a zero
is useful to define the sum over the empty set, so `AddRightCancelMonoid` is not enough. -/
class AddCancelMonoid (M : Type u) extends AddLeftCancelMonoid M, AddRightCancelMonoid M
Cancellative additive monoid
Informal description
An additive monoid in which addition is cancellative on both sides. This means that for any elements $a, b, c$ in the monoid, if $a + b = a + c$ or $b + a = c + a$, then $b = c$. Main examples include the natural numbers $\mathbb{N}$ and any additive group. This structure is particularly useful for sum lemmas, as the presence of a zero element allows defining sums over the empty set, which is not possible with just an `AddRightCancelMonoid`.
CancelMonoid structure
(M : Type u) extends LeftCancelMonoid M, RightCancelMonoid M
Full source 
/-- A monoid in which multiplication is cancellative. -/
@[to_additive]
class CancelMonoid (M : Type u) extends LeftCancelMonoid M, RightCancelMonoid M
Cancellative Monoid
Informal description
A monoid \( M \) in which multiplication is cancellative on both the left and the right. That is, for all \( a, b, c \in M \), if \( a \cdot b = a \cdot c \) or \( b \cdot a = c \cdot a \), then \( b = c \).
AddCancelCommMonoid structure
(M : Type u) extends AddCommMonoid M, AddLeftCancelMonoid M
Full source 
/-- Commutative version of `AddCancelMonoid`. -/
class AddCancelCommMonoid (M : Type u) extends AddCommMonoid M, AddLeftCancelMonoid M
Additive Cancellative Commutative Monoid
Informal description
An additive commutative monoid `M` where addition is left-cancelative (i.e., `a + b = a + c` implies `b = c` for all `a, b, c ∈ M`). This structure combines the properties of an additive commutative monoid and an additive left-cancelative monoid.
CancelCommMonoid structure
(M : Type u) extends CommMonoid M, LeftCancelMonoid M
Full source 
/-- Commutative version of `CancelMonoid`. -/
@[to_additive]
class CancelCommMonoid (M : Type u) extends CommMonoid M, LeftCancelMonoid M
Cancellative Commutative Monoid
Informal description
A commutative monoid `M` where the multiplication operation is cancellative, meaning that for any elements `a, b, c ∈ M`, if `a * b = a * c` or `b * a = c * a`, then `b = c`. This structure combines the properties of a commutative monoid and a left cancellative monoid.
CancelMonoid.toIsCancelMul instance
(M : Type u) [CancelMonoid M] : IsCancelMul M
Full source 
/-- Any `CancelMonoid G` satisfies `IsCancelMul G`. -/
@[to_additive toIsCancelAdd "Any `AddCancelMonoid G` satisfies `IsCancelAdd G`."]
instance (priority := 100) CancelMonoid.toIsCancelMul (M : Type u) [CancelMonoid M] :
    IsCancelMul M :=
  { mul_left_cancel := LeftCancelSemigroup.mul_left_cancel
    mul_right_cancel := RightCancelSemigroup.mul_right_cancel }
Cancellative Monoids Have Cancellative Multiplication
Informal description
Every cancellative monoid $M$ satisfies the cancellation property for multiplication. That is, for any elements $a, b, c \in M$, if $a \cdot b = a \cdot c$ or $b \cdot a = c \cdot a$, then $b = c$.
InvolutiveNeg structure
(A : Type*) extends Neg A
Full source 
/-- Auxiliary typeclass for types with an involutive `Neg`. -/
class InvolutiveNeg (A : Type*) extends Neg A where
  protected neg_neg : ∀ x : A, - -x = x
Involutive Negation
Informal description
The structure `InvolutiveNeg` represents types equipped with a negation operation that is involutive, meaning applying the negation twice returns the original element. Formally, for any element $a$ of type $A$, we have $-(-a) = a$.
InvolutiveInv structure
(G : Type*) extends Inv G
Full source 
/-- Auxiliary typeclass for types with an involutive `Inv`. -/
@[to_additive]
class InvolutiveInv (G : Type*) extends Inv G where
  protected inv_inv : ∀ x : G, x⁻¹x⁻¹⁻¹ = x
Involutive Inversion Structure
Informal description
A structure for types equipped with an involutive inversion operation, meaning that applying the inversion operation twice returns the original element. That is, for any element $a$ of type $G$, we have $(a^{-1})^{-1} = a$.
inv_inv theorem
(a : G) : a⁻¹⁻¹ = a
Full source 
@[to_additive (attr := simp)]
theorem inv_inv (a : G) : a⁻¹a⁻¹⁻¹ = a :=
  InvolutiveInv.inv_inv _
Double Inversion Identity: $(a^{-1})^{-1} = a$
Informal description
For any element $a$ in a type $G$ equipped with an involutive inversion operation, the double inversion of $a$ equals $a$ itself, i.e., $(a^{-1})^{-1} = a$.
DivInvMonoid.div' definition
{G : Type u} [Monoid G] [Inv G] (a b : G) : G
Full source 
/-- In a class equipped with instances of both `Monoid` and `Inv`, this definition records what the
default definition for `Div` would be: `a * b⁻¹`.  This is later provided as the default value for
the `Div` instance in `DivInvMonoid`.

We keep it as a separate definition rather than inlining it in `DivInvMonoid` so that the `Div`
field of individual `DivInvMonoid`s constructed using that default value will not be unfolded at
`.instance` transparency. -/
def DivInvMonoid.div' {G : Type u} [Monoid G] [Inv G] (a b : G) : G := a * b⁻¹
Division in a monoid with inversion
Informal description
For a monoid \( G \) equipped with an inversion operation, the division of two elements \( a \) and \( b \) is defined as \( a \cdot b^{-1} \).
DivInvMonoid structure
(G : Type u) extends Monoid G, Inv G, Div G
Full source 
/-- A `DivInvMonoid` is a `Monoid` with operations `/` and `⁻¹` satisfying
`div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹`.

This deduplicates the name `div_eq_mul_inv`.
The default for `div` is such that `a / b = a * b⁻¹` holds by definition.

Adding `div` as a field rather than defining `a / b := a * b⁻¹` allows us to
avoid certain classes of unification failures, for example:
Let `Foo X` be a type with a `∀ X, Div (Foo X)` instance but no
`∀ X, Inv (Foo X)`, e.g. when `Foo X` is a `EuclideanDomain`. Suppose we
also have an instance `∀ X [Cromulent X], GroupWithZero (Foo X)`. Then the
`(/)` coming from `GroupWithZero.div` cannot be definitionally equal to
the `(/)` coming from `Foo.Div`.

In the same way, adding a `zpow` field makes it possible to avoid definitional failures
in diamonds. See the definition of `Monoid` and Note [forgetful inheritance] for more
explanations on this.
-/
class DivInvMonoid (G : Type u) extends Monoid G, Inv G, Div G where
  protected div := DivInvMonoid.div'
  /-- `a / b := a * b⁻¹` -/
  protected div_eq_mul_inv : ∀ a b : G, a / b = a * b⁻¹ := by intros; rfl
  /-- The power operation: `a ^ n = a * ··· * a`; `a ^ (-n) = a⁻¹ * ··· a⁻¹` (`n` times) -/
  protected zpow : ℤ → G → G := zpowRec npowRec
  /-- `a ^ 0 = 1` -/
  protected zpow_zero' : ∀ a : G, zpow 0 a = 1 := by intros; rfl
  /-- `a ^ (n + 1) = a ^ n * a` -/
  protected zpow_succ' (n : ℕ) (a : G) : zpow n.succ a = zpow n a * a := by
    intros; rfl
  /-- `a ^ -(n + 1) = (a ^ (n + 1))⁻¹` -/
  protected zpow_neg' (n : ℕ) (a : G) : zpow (Int.negSucc n) a = (zpow n.succ a)⁻¹ := by intros; rfl
Division-Inversion Monoid
Informal description
A `DivInvMonoid` is a structure extending a monoid with division and inversion operations, where division is defined in terms of multiplication and inversion as \( a / b = a * b^{-1} \). This setup avoids certain unification issues in typeclass inheritance scenarios.
SubNegMonoid.sub' definition
{G : Type u} [AddMonoid G] [Neg G] (a b : G) : G
Full source 
/-- In a class equipped with instances of both `AddMonoid` and `Neg`, this definition records what
the default definition for `Sub` would be: `a + -b`.  This is later provided as the default value
for the `Sub` instance in `SubNegMonoid`.

We keep it as a separate definition rather than inlining it in `SubNegMonoid` so that the `Sub`
field of individual `SubNegMonoid`s constructed using that default value will not be unfolded at
`.instance` transparency. -/
def SubNegMonoid.sub' {G : Type u} [AddMonoid G] [Neg G] (a b : G) : G := a + -b
Subtraction in an additive monoid with negation
Informal description
For an additive monoid \( G \) equipped with a negation operation, the subtraction of two elements \( a \) and \( b \) is defined as \( a + (-b) \).
SubNegMonoid structure
(G : Type u) extends AddMonoid G, Neg G, Sub G
Full source 
/-- A `SubNegMonoid` is an `AddMonoid` with unary `-` and binary `-` operations
satisfying `sub_eq_add_neg : ∀ a b, a - b = a + -b`.

The default for `sub` is such that `a - b = a + -b` holds by definition.

Adding `sub` as a field rather than defining `a - b := a + -b` allows us to
avoid certain classes of unification failures, for example:
Let `foo X` be a type with a `∀ X, Sub (Foo X)` instance but no
`∀ X, Neg (Foo X)`. Suppose we also have an instance
`∀ X [Cromulent X], AddGroup (Foo X)`. Then the `(-)` coming from
`AddGroup.sub` cannot be definitionally equal to the `(-)` coming from
`Foo.Sub`.

In the same way, adding a `zsmul` field makes it possible to avoid definitional failures
in diamonds. See the definition of `AddMonoid` and Note [forgetful inheritance] for more
explanations on this.
-/
class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
  protected sub := SubNegMonoid.sub'
  protected sub_eq_add_neg : ∀ a b : G, a - b = a + -b := by intros; rfl
  /-- Multiplication by an integer.
  Set this to `zsmulRec` unless `Module` diamonds are possible. -/
  protected zsmul : ℤ → G → G
  protected zsmul_zero' : ∀ a : G, zsmul 0 a = 0 := by intros; rfl
  protected zsmul_succ' (n : ℕ) (a : G) :
      zsmul n.succ a = zsmul n a + a := by
    intros; rfl
  protected zsmul_neg' (n : ℕ) (a : G) : zsmul (Int.negSucc n) a = -zsmul n.succ a := by
    intros; rfl
Subtraction-Negation Monoid
Informal description
A `SubNegMonoid` is an additive monoid `G` equipped with a unary negation operation `-` and a binary subtraction operation `-`, satisfying the identity `a - b = a + (-b)` for all `a, b ∈ G`. The subtraction operation is defined in terms of addition and negation by default to avoid unification issues in certain contexts.
SubNegMonoid.toZSMul instance
{M} [SubNegMonoid M] : SMul ℤ M
Full source 
instance SubNegMonoid.toZSMul {M} [SubNegMonoid M] : SMul ℤ M :=
  ⟨SubNegMonoid.zsmul⟩
Integer Scalar Multiplication in Subtraction-Negation Monoids
Informal description
For any subtraction-negation monoid $M$, there is a canonical scalar multiplication operation $\mathbb{Z} \times M \to M$ defined on $M$.
IsAddCyclic structure
(G : Type u) [SMul ℤ G]
Full source 
/-- A group is called *cyclic* if it is generated by a single element. -/
class IsAddCyclic (G : Type u) [SMul ℤ G] : Prop where
  protected exists_zsmul_surjective : ∃ g : G, Function.Surjective (· • g : ℤ → G)
Cyclic group
Informal description
A group $G$ is called *cyclic* if there exists an element $g \in G$ such that every element of $G$ can be written as $g^n$ for some integer $n$. In additive notation, this means every element can be written as $n \cdot g$ for some integer $n$.
IsCyclic structure
(G : Type u) [Pow G ℤ]
Full source 
/-- A group is called *cyclic* if it is generated by a single element. -/
@[to_additive]
class IsCyclic (G : Type u) [Pow G ℤ] : Prop where
  protected exists_zpow_surjective : ∃ g : G, Function.Surjective (g ^ · : ℤ → G)
Cyclic group
Informal description
A group $G$ is called *cyclic* if there exists an element $g \in G$ such that every element of $G$ can be written as $g^n$ for some integer $n$. In other words, $G$ is generated by a single element $g$.
exists_zpow_surjective theorem
(G : Type*) [Pow G ℤ] [IsCyclic G] : ∃ g : G, Function.Surjective (g ^ · : ℤ → G)
Full source 
@[to_additive]
theorem exists_zpow_surjective (G : Type*) [Pow G ℤ] [IsCyclic G] :
    ∃ g : G, Function.Surjective (g ^ · : ℤ → G) :=
  IsCyclic.exists_zpow_surjective
Existence of a Generator for Cyclic Groups via Integer Powers
Informal description
For any cyclic group $G$ with integer exponentiation, there exists an element $g \in G$ such that the function $n \mapsto g^n$ from the integers $\mathbb{Z}$ to $G$ is surjective. In other words, every element of $G$ can be expressed as $g^n$ for some integer $n$.
zpow_eq_pow theorem
(n : ℤ) (x : G) : DivInvMonoid.zpow n x = x ^ n
Full source 
@[to_additive (attr := simp) zsmul_eq_smul] theorem zpow_eq_pow (n : ℤ) (x : G) :
    DivInvMonoid.zpow n x = x ^ n :=
  rfl
Equivalence of Integer Power Operations: $\text{zpow}(n, x) = x^n$
Informal description
For any integer $n$ and any element $x$ in a division-inversion monoid $G$, the integer power operation `DivInvMonoid.zpow` applied to $n$ and $x$ is equal to $x$ raised to the power $n$, i.e., $x^n$.
zpow_zero theorem
(a : G) : a ^ (0 : ℤ) = 1
Full source 
@[to_additive (attr := simp) zero_zsmul] theorem zpow_zero (a : G) : a ^ (0 : ℤ) = 1 :=
  DivInvMonoid.zpow_zero' a
Zero Exponent Law: $a^0 = 1$ in Division-Inversion Monoids
Informal description
For any element $a$ in a division-inversion monoid $G$, raising $a$ to the integer power $0$ yields the multiplicative identity $1$, i.e., $a^0 = 1$.
zpow_natCast theorem
(a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
Full source 
@[to_additive (attr := simp, norm_cast) natCast_zsmul]
theorem zpow_natCast (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
  | 0 => (zpow_zero _).trans (pow_zero _).symm
  | n + 1 => calc
    a ^ (↑(n + 1) : ℤ) = a ^ (n : ℤ) * a := DivInvMonoid.zpow_succ' _ _
    _ = a ^ n * a := congrArg (· * a) (zpow_natCast a n)
    _ = a ^ (n + 1) := (pow_succ _ _).symm
Equality of Integer and Natural Powers: $a^{(n : \mathbb{Z})} = a^n$
Informal description
For any element $a$ in a division-inversion monoid $G$ and any natural number $n$, the integer power $a^n$ (where $n$ is interpreted as an integer) is equal to the natural number power $a^n$ (where $n$ is interpreted as a natural number).
zpow_ofNat theorem
(a : G) (n : ℕ) : a ^ (ofNat(n) : ℤ) = a ^ OfNat.ofNat n
Full source 
@[to_additive ofNat_zsmul]
lemma zpow_ofNat (a : G) (n : ℕ) : a ^ (ofNat(n) : ℤ) = a ^ OfNat.ofNat n :=
  zpow_natCast ..
Equality of Integer and Natural Powers: $a^{(n : \mathbb{Z})} = a^n$
Informal description
For any element $a$ in a division-inversion monoid $G$ and any natural number $n$, the integer power $a^{(n : \mathbb{Z})}$ is equal to the natural number power $a^n$.
zpow_negSucc theorem
(a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹
Full source 
theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹ := by
  rw [← zpow_natCast]
  exact DivInvMonoid.zpow_neg' n a
Negative Successor Power Equals Inverse of Successor Power: $a^{-(n+1)} = (a^{n+1})^{-1}$
Informal description
For any element $a$ in a division-inversion monoid $G$ and any natural number $n$, the integer power $a^{-(n+1)}$ is equal to the inverse of $a^{n+1}$, i.e., $a^{-(n+1)} = (a^{n+1})^{-1}$.
negSucc_zsmul theorem
{G} [SubNegMonoid G] (a : G) (n : ℕ) : Int.negSucc n • a = -((n + 1) • a)
Full source 
theorem negSucc_zsmul {G} [SubNegMonoid G] (a : G) (n : ℕ) :
    Int.negSucc n • a = -((n + 1) • a) := by
  rw [← natCast_zsmul]
  exact SubNegMonoid.zsmul_neg' n a
Scalar Multiplication by Negative Successor: $(-(n + 1)) \cdot a = -((n + 1) \cdot a)$
Informal description
For any element $a$ in a subtraction-negation monoid $G$ and any natural number $n$, the scalar multiplication of $a$ by the negative integer $- (n + 1)$ is equal to the negation of the scalar multiplication of $a$ by $n + 1$, i.e., $(-(n + 1)) \cdot a = -((n + 1) \cdot a)$.
div_eq_mul_inv theorem
(a b : G) : a / b = a * b⁻¹
Full source 
/-- Dividing by an element is the same as multiplying by its inverse.

This is a duplicate of `DivInvMonoid.div_eq_mul_inv` ensuring that the types unfold better.
-/
@[to_additive "Subtracting an element is the same as adding by its negative.
This is a duplicate of `SubNegMonoid.sub_eq_add_neg` ensuring that the types unfold better."]
theorem div_eq_mul_inv (a b : G) : a / b = a * b⁻¹ :=
  DivInvMonoid.div_eq_mul_inv _ _
Division as Multiplication by Inverse in a Division-Inversion Monoid
Informal description
For any elements $a$ and $b$ in a division-inversion monoid $G$, the division operation satisfies $a / b = a \cdot b^{-1}$.
inv_eq_one_div theorem
(x : G) : x⁻¹ = 1 / x
Full source 
@[to_additive, field_simps] -- The attributes are out of order on purpose
theorem inv_eq_one_div (x : G) : x⁻¹ = 1 / x := by rw [div_eq_mul_inv, one_mul]
Inverse as One Divided by Element: $x^{-1} = 1 / x$
Informal description
For any element $x$ in a division-inversion monoid $G$, the inverse of $x$ is equal to $1$ divided by $x$, i.e., $x^{-1} = 1 / x$.
mul_div_assoc theorem
(a b c : G) : a * b / c = a * (b / c)
Full source 
@[to_additive]
theorem mul_div_assoc (a b c : G) : a * b / c = a * (b / c) := by
  rw [div_eq_mul_inv, div_eq_mul_inv, mul_assoc _ _ _]
Associativity of Multiplication and Division in a Division-Inversion Monoid
Informal description
For any elements $a, b, c$ in a division-inversion monoid $G$, the operation satisfies $a \cdot b / c = a \cdot (b / c)$.
one_div theorem
(a : G) : 1 / a = a⁻¹
Full source 
@[to_additive (attr := simp)]
theorem one_div (a : G) : 1 / a = a⁻¹ :=
  (inv_eq_one_div a).symm
Reciprocal as Inverse: $1/a = a^{-1}$
Informal description
For any element $a$ in a division-inversion monoid $G$, the reciprocal of $a$ is equal to the inverse of $a$, i.e., $1 / a = a^{-1}$.
zpow_one theorem
(a : G) : a ^ (1 : ℤ) = a
Full source 
@[to_additive (attr := simp) one_zsmul]
lemma zpow_one (a : G) : a ^ (1 : ℤ) = a := by rw [zpow_ofNat, pow_one]
First Integer Power Identity: $a^1 = a$
Informal description
For any element $a$ in a division-inversion monoid $G$, the first integer power of $a$ equals $a$ itself, i.e., $a^1 = a$.
zpow_two theorem
(a : G) : a ^ (2 : ℤ) = a * a
Full source 
@[to_additive two_zsmul] lemma zpow_two (a : G) : a ^ (2 : ℤ) = a * a := by rw [zpow_ofNat, pow_two]
Square of an Element in a Division-Inversion Monoid: $a^2 = a \cdot a$
Informal description
For any element $a$ in a division-inversion monoid $G$, the integer power $a^2$ equals $a$ multiplied by itself, i.e., $a^2 = a \cdot a$.
zpow_neg_one theorem
(x : G) : x ^ (-1 : ℤ) = x⁻¹
Full source 
@[to_additive neg_one_zsmul]
lemma zpow_neg_one (x : G) : x ^ (-1 : ℤ) = x⁻¹ :=
  (zpow_negSucc x 0).trans <| congr_arg Inv.inv (pow_one x)
Negative One Power Equals Inverse: $x^{-1} = x^{-1}$
Informal description
For any element $x$ in a division-inversion monoid $G$, the integer power $x^{-1}$ is equal to the inverse of $x$, i.e., $x^{-1} = x^{-1}$.
zpow_neg_coe_of_pos theorem
(a : G) : ∀ {n : ℕ}, 0 < n → a ^ (-(n : ℤ)) = (a ^ n)⁻¹
Full source 
@[to_additive]
lemma zpow_neg_coe_of_pos (a : G) : ∀ {n : ℕ}, 0 < n → a ^ (-(n : ℤ)) = (a ^ n)⁻¹
  | _ + 1, _ => zpow_negSucc _ _
Negative Integer Power Equals Inverse of Positive Power: $a^{-n} = (a^n)^{-1}$ for $n > 0$
Informal description
For any element $a$ in a division-inversion monoid $G$ and any positive natural number $n$, the integer power $a^{-n}$ is equal to the inverse of $a^n$, i.e., $a^{-n} = (a^n)^{-1}$.
NegZeroClass structure
(G : Type*) extends Zero G, Neg G
Full source 
/-- Typeclass for expressing that `-0 = 0`. -/
class NegZeroClass (G : Type*) extends Zero G, Neg G where
  protected neg_zero : -(0 : G) = 0
Negation-Zero Class
Informal description
A structure `NegZeroClass G` consists of a type `G` equipped with a zero element `0` and a negation operation `-`, satisfying the axiom that the negation of zero is zero: $-0 = 0$.
SubNegZeroMonoid structure
(G : Type*) extends SubNegMonoid G, NegZeroClass G
Full source 
/-- A `SubNegMonoid` where `-0 = 0`. -/
class SubNegZeroMonoid (G : Type*) extends SubNegMonoid G, NegZeroClass G
Subtraction-Negation-Zero Monoid
Informal description
A `SubNegZeroMonoid` is an algebraic structure that combines the properties of a `SubNegMonoid` (a structure with subtraction and negation operations) and a `NegZeroClass` (a structure where the negation of zero is zero). Specifically, it ensures that the negation of the zero element is itself zero, i.e., $-0 = 0$, while maintaining the subtraction and negation operations inherited from `SubNegMonoid`.
InvOneClass structure
(G : Type*) extends One G, Inv G
Full source 
/-- Typeclass for expressing that `1⁻¹ = 1`. -/
@[to_additive]
class InvOneClass (G : Type*) extends One G, Inv G where
  protected inv_one : (1 : G)⁻¹ = 1
Inverse of One is One
Informal description
The structure `InvOneClass` expresses that the inverse of the multiplicative identity element $1$ in a type $G$ is itself $1$, i.e., $1^{-1} = 1$. This structure extends the `One` and `Inv` classes, which provide the identity element and the inverse operation, respectively.
DivInvOneMonoid structure
(G : Type*) extends DivInvMonoid G, InvOneClass G
Full source 
/-- A `DivInvMonoid` where `1⁻¹ = 1`. -/
@[to_additive]
class DivInvOneMonoid (G : Type*) extends DivInvMonoid G, InvOneClass G
DivInvOneMonoid
Informal description
A `DivInvOneMonoid` is a structure that extends a `DivInvMonoid` with the additional property that the inverse of the multiplicative identity element is itself. In other words, it satisfies $1^{-1} = 1$ for the identity element $1$ of the monoid.
inv_one theorem
: (1 : G)⁻¹ = 1
Full source 
@[to_additive (attr := simp)]
theorem inv_one : (1 : G)⁻¹ = 1 :=
  InvOneClass.inv_one
Inverse of One is One
Informal description
In any type $G$ with a multiplicative identity element $1$ and an inversion operation, the inverse of $1$ is itself, i.e., $1^{-1} = 1$.
SubtractionMonoid structure
(G : Type u) extends SubNegMonoid G, InvolutiveNeg G
Full source 
/-- A `SubtractionMonoid` is a `SubNegMonoid` with involutive negation and such that
`-(a + b) = -b + -a` and `a + b = 0 → -a = b`. -/
class SubtractionMonoid (G : Type u) extends SubNegMonoid G, InvolutiveNeg G where
  protected neg_add_rev (a b : G) : -(a + b) = -b + -a
  /-- Despite the asymmetry of `neg_eq_of_add`, the symmetric version is true thanks to the
  involutivity of negation. -/
  protected neg_eq_of_add (a b : G) : a + b = 0 → -a = b
Subtraction Monoid
Informal description
A `SubtractionMonoid` is an additive structure `G` equipped with a subtraction operation and negation, where the negation is involutive (i.e., `-(-a) = a` for all `a ∈ G`), and satisfies the properties: 1. `-(a + b) = -b + -a` for all `a, b ∈ G`, 2. If `a + b = 0`, then `-a = b`. This structure extends `SubNegMonoid` (which provides subtraction and negation) and `InvolutiveNeg` (which ensures the negation is involutive).
DivisionMonoid structure
(G : Type u) extends DivInvMonoid G, InvolutiveInv G
Full source 
/-- A `DivisionMonoid` is a `DivInvMonoid` with involutive inversion and such that
`(a * b)⁻¹ = b⁻¹ * a⁻¹` and `a * b = 1 → a⁻¹ = b`.

This is the immediate common ancestor of `Group` and `GroupWithZero`. -/
@[to_additive]
class DivisionMonoid (G : Type u) extends DivInvMonoid G, InvolutiveInv G where
  protected mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹
  /-- Despite the asymmetry of `inv_eq_of_mul`, the symmetric version is true thanks to the
  involutivity of inversion. -/
  protected inv_eq_of_mul (a b : G) : a * b = 1 → a⁻¹ = b
Division Monoid
Informal description
A division monoid is a structure extending a `DivInvMonoid` with an involutive inversion operation (i.e., $(a^{-1})^{-1} = a$) and satisfying the properties: 1. The inverse of a product is the reverse product of inverses: $(a \cdot b)^{-1} = b^{-1} \cdot a^{-1}$. 2. If $a \cdot b = 1$, then $a^{-1} = b$. This structure serves as a common generalization of groups and groups with zero.
mul_inv_rev theorem
(a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹
Full source 
@[to_additive (attr := simp) neg_add_rev]
theorem mul_inv_rev (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
  DivisionMonoid.mul_inv_rev _ _
Inverse of Product Equals Reverse Product of Inverses
Informal description
For any elements $a$ and $b$ in a division monoid $G$, the inverse of the product $a \cdot b$ is equal to the product of the inverses in reverse order, i.e., $(a \cdot b)^{-1} = b^{-1} \cdot a^{-1}$.
inv_eq_of_mul_eq_one_right theorem
: a * b = 1 → a⁻¹ = b
Full source 
@[to_additive]
theorem inv_eq_of_mul_eq_one_right : a * b = 1 → a⁻¹ = b :=
  DivisionMonoid.inv_eq_of_mul _ _
Inverse Characterization from Right Multiplication Identity
Informal description
For any elements $a$ and $b$ in a division monoid $G$, if $a \cdot b = 1$, then the inverse of $a$ is equal to $b$.
inv_eq_of_mul_eq_one_left theorem
(h : a * b = 1) : b⁻¹ = a
Full source 
@[to_additive]
theorem inv_eq_of_mul_eq_one_left (h : a * b = 1) : b⁻¹ = a := by
  rw [← inv_eq_of_mul_eq_one_right h, inv_inv]
Inverse Characterization from Left Multiplication Identity
Informal description
For any elements $a$ and $b$ in a division monoid $G$, if $a \cdot b = 1$, then the inverse of $b$ is equal to $a$.
SubtractionCommMonoid structure
(G : Type u) extends SubtractionMonoid G, AddCommMonoid G
Full source 
/-- Commutative `SubtractionMonoid`. -/
class SubtractionCommMonoid (G : Type u) extends SubtractionMonoid G, AddCommMonoid G
Commutative Subtraction Monoid
Informal description
A commutative subtraction monoid is an additive commutative monoid `G` equipped with a subtraction operation that satisfies the axioms of a subtraction monoid. This structure combines the properties of an additive commutative monoid with those of a subtraction monoid, which includes a pseudo-inverse operation that interacts appropriately with the addition operation.
DivisionCommMonoid structure
(G : Type u) extends DivisionMonoid G, CommMonoid G
Full source 
/-- Commutative `DivisionMonoid`.

This is the immediate common ancestor of `CommGroup` and `CommGroupWithZero`. -/
@[to_additive SubtractionCommMonoid]
class DivisionCommMonoid (G : Type u) extends DivisionMonoid G, CommMonoid G
Commutative Division Monoid
Informal description
A commutative division monoid is an algebraic structure that extends both a division monoid and a commutative monoid. It serves as the immediate common ancestor of commutative groups and commutative groups with zero. The structure combines the properties of division (pseudo-inversion) with commutativity of the binary operation.
Group structure
(G : Type u) extends DivInvMonoid G
Full source 
/-- A `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.

There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.

Use `Group.ofLeftAxioms` or `Group.ofRightAxioms` to define a group structure
on a type with the minimum proof obligations.
-/
class Group (G : Type u) extends DivInvMonoid G where
  protected inv_mul_cancel : ∀ a : G, a⁻¹ * a = 1
Group
Informal description
A group is a monoid equipped with an inversion operation $^{-1}$ satisfying the left inverse property $a^{-1} * a = 1$ for every element $a$. It also has a division operation $/$ defined by $a / b = a * b^{-1}$ by default.
AddGroup structure
(A : Type u) extends SubNegMonoid A
Full source 
/-- An `AddGroup` is an `AddMonoid` with a unary `-` satisfying `-a + a = 0`.

There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.

Use `AddGroup.ofLeftAxioms` or `AddGroup.ofRightAxioms` to define an
additive group structure on a type with the minimum proof obligations.
-/
class AddGroup (A : Type u) extends SubNegMonoid A where
  protected neg_add_cancel : ∀ a : A, -a + a = 0
Additive Group
Informal description
An additive group is an additive monoid equipped with a unary negation operation `-` satisfying the property that for any element `a`, the sum of `-a` and `a` is the additive identity `0`. Additionally, it includes a binary subtraction operation `-` defined as `a - b = a + (-b)`, with this equality holding by definition.
inv_mul_cancel theorem
(a : G) : a⁻¹ * a = 1
Full source 
@[to_additive (attr := simp)]
theorem inv_mul_cancel (a : G) : a⁻¹ * a = 1 :=
  Group.inv_mul_cancel a
Inverse Multiplication Cancellation: $a^{-1} \cdot a = 1$
Informal description
For any element $a$ in a group $G$, the product of its inverse $a^{-1}$ with $a$ equals the identity element $1$, i.e., $a^{-1} \cdot a = 1$.
mul_inv_cancel theorem
(a : G) : a * a⁻¹ = 1
Full source 
@[to_additive (attr := simp)]
theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1 := by
  rw [← inv_mul_cancel a⁻¹, inv_eq_of_mul (inv_mul_cancel a)]
Multiplication-Inverse Cancellation: $a \cdot a^{-1} = 1$
Informal description
For any element $a$ in a group $G$, the product of $a$ with its inverse $a^{-1}$ equals the identity element $1$, i.e., $a \cdot a^{-1} = 1$.
div_self' theorem
(a : G) : a / a = 1
Full source 
@[to_additive (attr := simp) sub_self]
theorem div_self' (a : G) : a / a = 1 := by rw [div_eq_mul_inv, mul_inv_cancel a]
Division of an Element by Itself Yields the Identity: $a / a = 1$
Informal description
For any element $a$ in a group $G$, the division of $a$ by itself equals the identity element, i.e., $a / a = 1$.
inv_mul_cancel_left theorem
(a b : G) : a⁻¹ * (a * b) = b
Full source 
@[to_additive (attr := simp)]
theorem inv_mul_cancel_left (a b : G) : a⁻¹ * (a * b) = b := by
  rw [← mul_assoc, inv_mul_cancel, one_mul]
Left cancellation via inverse multiplication: $a^{-1}(ab) = b$
Informal description
For any elements $a$ and $b$ in a group $G$, the product of the inverse of $a$ with the product of $a$ and $b$ equals $b$, i.e., $a^{-1} \cdot (a \cdot b) = b$.
mul_inv_cancel_left theorem
(a b : G) : a * (a⁻¹ * b) = b
Full source 
@[to_additive (attr := simp)]
theorem mul_inv_cancel_left (a b : G) : a * (a⁻¹ * b) = b := by
  rw [← mul_assoc, mul_inv_cancel, one_mul]
Left cancellation via inverse multiplication: $a \cdot (a^{-1} \cdot b) = b$
Informal description
For any elements $a$ and $b$ in a group $G$, the product $a \cdot (a^{-1} \cdot b)$ equals $b$.
mul_inv_cancel_right theorem
(a b : G) : a * b * b⁻¹ = a
Full source 
@[to_additive (attr := simp)]
theorem mul_inv_cancel_right (a b : G) : a * b * b⁻¹ = a := by
  rw [mul_assoc, mul_inv_cancel, mul_one]
Right multiplication-inverse cancellation: $a \cdot b \cdot b^{-1} = a$
Informal description
For any elements $a$ and $b$ in a group $G$, the product $a \cdot b \cdot b^{-1}$ equals $a$.
mul_div_cancel_right theorem
(a b : G) : a * b / b = a
Full source 
@[to_additive (attr := simp)]
theorem mul_div_cancel_right (a b : G) : a * b / b = a := by
  rw [div_eq_mul_inv, mul_inv_cancel_right a b]
Right Division-Multiplication Cancellation: $(a \cdot b)/b = a$
Informal description
For any elements $a$ and $b$ in a group $G$, the operation $(a \cdot b) / b$ equals $a$.
inv_mul_cancel_right theorem
(a b : G) : a * b⁻¹ * b = a
Full source 
@[to_additive (attr := simp)]
theorem inv_mul_cancel_right (a b : G) : a * b⁻¹ * b = a := by
  rw [mul_assoc, inv_mul_cancel, mul_one]
Right inverse multiplication cancellation: $a \cdot b^{-1} \cdot b = a$
Informal description
For any elements $a$ and $b$ in a group $G$, the product $a \cdot b^{-1} \cdot b$ equals $a$.
div_mul_cancel theorem
(a b : G) : a / b * b = a
Full source 
@[to_additive (attr := simp)]
theorem div_mul_cancel (a b : G) : a / b * b = a := by
  rw [div_eq_mul_inv, inv_mul_cancel_right a b]
Division-Multiplication Cancellation: $(a / b) \cdot b = a$
Informal description
For any elements $a$ and $b$ in a group $G$, the operation $(a / b) \cdot b$ equals $a$.
Group.toDivisionMonoid instance
: DivisionMonoid G
Full source 
@[to_additive]
instance (priority := 100) Group.toDivisionMonoid : DivisionMonoid G :=
  { inv_inv := fun a ↦ inv_eq_of_mul (inv_mul_cancel a)
    mul_inv_rev :=
      fun a b ↦ inv_eq_of_mul <| by rw [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]
    inv_eq_of_mul := fun _ _ ↦ inv_eq_of_mul }
Groups are Division Monoids
Informal description
Every group $G$ is a division monoid. That is, the group structure on $G$ induces a division monoid structure where the inversion operation is involutive and satisfies $(a \cdot b)^{-1} = b^{-1} \cdot a^{-1}$ for all $a, b \in G$, and if $a \cdot b = 1$ then $a^{-1} = b$.
Group.toCancelMonoid instance
: CancelMonoid G
Full source 
@[to_additive]
instance (priority := 100) Group.toCancelMonoid : CancelMonoid G :=
  { ‹Group G› with
    mul_right_cancel := fun a b c h ↦ by rw [← mul_inv_cancel_right a b, h, mul_inv_cancel_right]
    mul_left_cancel := fun a b c h ↦ by rw [← inv_mul_cancel_left a b, h, inv_mul_cancel_left] }
Groups are Cancellative Monoids
Informal description
Every group $G$ is a cancellative monoid. That is, the group structure on $G$ ensures that multiplication is cancellative on both the left and the right.
AddCommGroup structure
(G : Type u) extends AddGroup G, AddCommMonoid G
Full source 
/-- An additive commutative group is an additive group with commutative `(+)`. -/
class AddCommGroup (G : Type u) extends AddGroup G, AddCommMonoid G
Additive Commutative Group
Informal description
An additive commutative group is a structure that extends an additive group with the additional property that the binary operation is commutative. In other words, it is an additive group where the operation $+$ satisfies $a + b = b + a$ for all elements $a, b$ in the group.
CommGroup structure
(G : Type u) extends Group G, CommMonoid G
Full source 
/-- A commutative group is a group with commutative `(*)`. -/
@[to_additive]
class CommGroup (G : Type u) extends Group G, CommMonoid G
Commutative Group
Informal description
A commutative group is a group structure on a type $G$ where the binary operation is commutative. That is, for all $x, y \in G$, we have $x * y = y * x$.
CommGroup.toCancelCommMonoid instance
: CancelCommMonoid G
Full source 
@[to_additive]
instance (priority := 100) CommGroup.toCancelCommMonoid : CancelCommMonoid G :=
  { ‹CommGroup G›, Group.toCancelMonoid with }
Commutative Groups are Cancellative Commutative Monoids
Informal description
Every commutative group $G$ is a cancellative commutative monoid. That is, the commutative group structure on $G$ ensures that the multiplication operation is both commutative and cancellative.
CommGroup.toDivisionCommMonoid instance
: DivisionCommMonoid G
Full source 
@[to_additive]
instance (priority := 100) CommGroup.toDivisionCommMonoid : DivisionCommMonoid G :=
  { ‹CommGroup G›, Group.toDivisionMonoid with }
Commutative Groups are Commutative Division Monoids
Informal description
Every commutative group $G$ is a commutative division monoid. That is, the commutative group structure on $G$ induces a commutative division monoid structure where the inversion operation is involutive and satisfies $(a \cdot b)^{-1} = b^{-1} \cdot a^{-1}$ for all $a, b \in G$, and if $a \cdot b = 1$ then $a^{-1} = b$.
inv_mul_cancel_comm theorem
(a b : G) : a⁻¹ * b * a = b
Full source 
@[to_additive (attr := simp)] lemma inv_mul_cancel_comm (a b : G) : a⁻¹ * b * a = b := by
  rw [mul_comm, mul_inv_cancel_left]
Conjugation Cancellation in Commutative Groups: $a^{-1} b a = b$
Informal description
For any elements $a$ and $b$ in a commutative group $G$, the product $a^{-1} \cdot b \cdot a$ equals $b$.
mul_inv_cancel_comm theorem
(a b : G) : a * b * a⁻¹ = b
Full source 
@[to_additive (attr := simp)]
lemma mul_inv_cancel_comm (a b : G) : a * b * a⁻¹ = b := by rw [mul_comm, inv_mul_cancel_left]
Conjugation Cancellation in Commutative Groups: $aba^{-1} = b$
Informal description
For any elements $a$ and $b$ in a commutative group $G$, the product $a \cdot b \cdot a^{-1}$ equals $b$.
inv_mul_cancel_comm_assoc theorem
(a b : G) : a⁻¹ * (b * a) = b
Full source 
@[to_additive (attr := simp)] lemma inv_mul_cancel_comm_assoc (a b : G) : a⁻¹ * (b * a) = b := by
  rw [mul_comm, mul_inv_cancel_right]
Commutative conjugation identity: $a^{-1}(b a) = b$
Informal description
For any elements $a$ and $b$ in a commutative group $G$, the product $a^{-1} \cdot (b \cdot a)$ equals $b$.
mul_inv_cancel_comm_assoc theorem
(a b : G) : a * (b * a⁻¹) = b
Full source 
@[to_additive (attr := simp)] lemma mul_inv_cancel_comm_assoc (a b : G) : a * (b * a⁻¹) = b := by
  rw [mul_comm, inv_mul_cancel_right]
Commutative cancellation: $a \cdot (b \cdot a^{-1}) = b$
Informal description
For any elements $a$ and $b$ in a commutative group $G$, the product $a \cdot (b \cdot a^{-1})$ equals $b$.
IsAddCommutative structure
(M : Type*) [Add M]
Full source 
/-- A Prop stating that the addition is commutative. -/
class IsAddCommutative (M : Type*) [Add M] : Prop where
  is_comm : Std.Commutative (α := M) (· + ·)
Commutativity of addition
Informal description
A property stating that the addition operation on a type `M` is commutative, i.e., for any two elements `a` and `b` in `M`, we have `a + b = b + a`.
IsMulCommutative structure
(M : Type*) [Mul M]
Full source 
/-- A Prop stating that the multiplication is commutative. -/
@[to_additive]
class IsMulCommutative (M : Type*) [Mul M] : Prop where
  is_comm : Std.Commutative (α := M) (· * ·)
Commutativity of multiplication
Informal description
A property stating that the binary operation $\cdot$ on a type $M$ equipped with a multiplication is commutative, i.e., for all $a, b \in M$, $a \cdot b = b \cdot a$.
CommGroup.ofIsMulCommutative instance
{G : Type*} [Group G] [IsMulCommutative G] : CommGroup G
Full source 
@[to_additive]
instance (priority := 100) CommGroup.ofIsMulCommutative {G : Type*} [Group G] [IsMulCommutative G] :
    CommGroup G where
Commutative Group from Commutative Multiplication
Informal description
Every group $G$ with a commutative multiplication operation is a commutative group.