doc-next-gen

Mathlib.Algebra.Group.Basic

Module docstring

{"# Basic lemmas about semigroups, monoids, and groups

This file lists various basic lemmas about semigroups, monoids, and groups. Most proofs are one-liners from the corresponding axioms. For the definitions of semigroups, monoids and groups, see Algebra/Group/Defs.lean. "}

pow_dite theorem
(p : Prop) [Decidable p] (a : α) (b : p → β) (c : ¬p → β) : a ^ (if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h
Full source 
@[to_additive (attr := simp) dite_smul]
lemma pow_dite (p : Prop) [Decidable p] (a : α) (b : p → β) (c : ¬ p → β) :
    a ^ (if h : p then b h else c h) = if h : p then a ^ b h else a ^ c h := by split_ifs <;> rfl
Power of Conditional Expression via Dependent If-Then-Else
Informal description
Let $p$ be a decidable proposition, $a$ an element of type $\alpha$, and $b : p \to \beta$, $c : \lnot p \to \beta$ functions. Then the power operation satisfies: $$ a^{(if\ h : p\ then\ b(h)\ else\ c(h))} = if\ h : p\ then\ a^{b(h)}\ else\ a^{c(h)} $$
dite_pow theorem
(p : Prop) [Decidable p] (a : p → α) (b : ¬p → α) (c : β) : (if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c
Full source 
@[to_additive (attr := simp) smul_dite]
lemma dite_pow (p : Prop) [Decidable p] (a : p → α) (b : ¬ p → α) (c : β) :
    (if h : p then a h else b h) ^ c = if h : p then a h ^ c else b h ^ c := by split_ifs <;> rfl
Power of Conditional Expression in Groups
Informal description
Let $p$ be a decidable proposition, and let $a : p \to \alpha$ and $b : \neg p \to \alpha$ be functions. Then for any exponent $c : \beta$, the power of the conditional expression $\text{if } h : p \text{ then } a(h) \text{ else } b(h)$ raised to $c$ is equal to the conditional expression $\text{if } h : p \text{ then } a(h)^c \text{ else } b(h)^c$.
pow_ite theorem
(p : Prop) [Decidable p] (a : α) (b c : β) : a ^ (if p then b else c) = if p then a ^ b else a ^ c
Full source 
@[to_additive (attr := simp) ite_smul]
lemma pow_ite (p : Prop) [Decidable p] (a : α) (b c : β) :
    a ^ (if p then b else c) = if p then a ^ b else a ^ c := pow_dite _ _ _ _
Power of Conditional Expression via If-Then-Else
Informal description
Let $p$ be a decidable proposition, $a$ an element of type $\alpha$, and $b, c$ elements of type $\beta$. Then the power operation satisfies: $$ a^{(if\ p\ then\ b\ else\ c)} = if\ p\ then\ a^b\ else\ a^c $$
ite_pow theorem
(p : Prop) [Decidable p] (a b : α) (c : β) : (if p then a else b) ^ c = if p then a ^ c else b ^ c
Full source 
@[to_additive (attr := simp) smul_ite]
lemma ite_pow (p : Prop) [Decidable p] (a b : α) (c : β) :
    (if p then a else b) ^ c = if p then a ^ c else b ^ c := dite_pow _ _ _ _
Power of Conditional Expression in Groups
Informal description
Let $p$ be a decidable proposition, and let $a, b$ be elements of a group $\alpha$. Then for any exponent $c$ in $\beta$, the power of the conditional expression $\text{if } p \text{ then } a \text{ else } b$ raised to $c$ is equal to the conditional expression $\text{if } p \text{ then } a^c \text{ else } b^c$. In symbols: $$(\text{if } p \text{ then } a \text{ else } b)^c = \text{if } p \text{ then } a^c \text{ else } b^c$$
Semigroup.to_isAssociative instance
: Std.Associative (α := α) (· * ·)
Full source 
@[to_additive]
instance Semigroup.to_isAssociative : Std.Associative (α := α) (· * ·) := ⟨mul_assoc⟩
Associativity of Multiplication in Semigroups
Informal description
For any semigroup $\alpha$, the multiplication operation $(\cdot * \cdot)$ is associative.
comp_mul_left theorem
(x y : α) : (x * ·) ∘ (y * ·) = (x * y * ·)
Full source 
/-- Composing two multiplications on the left by `y` then `x`
is equal to a multiplication on the left by `x * y`.
-/
@[to_additive (attr := simp) "Composing two additions on the left by `y` then `x`
is equal to an addition on the left by `x + y`."]
theorem comp_mul_left (x y : α) : (x * ·) ∘ (y * ·) = (x * y * ·) := by
  ext z
  simp [mul_assoc]
Composition of Left Multiplications in a Semigroup
Informal description
For any elements $x$ and $y$ in a semigroup $\alpha$, the composition of left multiplication by $x$ and left multiplication by $y$ is equal to left multiplication by $x * y$. In symbols: $$ (x \cdot \_) \circ (y \cdot \_) = (x * y \cdot \_) $$
comp_mul_right theorem
(x y : α) : (· * x) ∘ (· * y) = (· * (y * x))
Full source 
/-- Composing two multiplications on the right by `y` and `x`
is equal to a multiplication on the right by `y * x`.
-/
@[to_additive (attr := simp) "Composing two additions on the right by `y` and `x`
is equal to an addition on the right by `y + x`."]
theorem comp_mul_right (x y : α) : (· * x) ∘ (· * y) = (· * (y * x)) := by
  ext z
  simp [mul_assoc]
Composition of Right Multiplications in a Semigroup
Informal description
For any elements $x$ and $y$ in a semigroup $\alpha$, the composition of right multiplication by $y$ followed by right multiplication by $x$ is equal to right multiplication by $y * x$. In other words, the function composition $(\cdot * x) \circ (\cdot * y)$ equals the function $\cdot * (y * x)$.
CommMagma.to_isCommutative instance
[CommMagma G] : Std.Commutative (α := G) (· * ·)
Full source 
@[to_additive]
instance CommMagma.to_isCommutative [CommMagma G] : Std.Commutative (α := G) (· * ·) := ⟨mul_comm⟩
Commutativity of Multiplication in a Commutative Magma
Informal description
For any commutative magma $G$, the multiplication operation $(\cdot * \cdot)$ on $G$ is commutative.
ite_mul_one theorem
{P : Prop} [Decidable P] {a b : M} : ite P (a * b) 1 = ite P a 1 * ite P b 1
Full source 
@[to_additive]
theorem ite_mul_one {P : Prop} [Decidable P] {a b : M} :
    ite P (a * b) 1 = ite P a 1 * ite P b 1 := by
  by_cases h : P <;> simp [h]
Conditional Product Identity in Monoids: $\text{ite}(P, a * b, 1) = \text{ite}(P, a, 1) * \text{ite}(P, b, 1)$
Informal description
For any proposition $P$ with a decidable instance, and for any elements $a, b$ in a monoid $M$, the conditional expression $\text{ite}(P, a * b, 1)$ is equal to the product of the conditional expressions $\text{ite}(P, a, 1)$ and $\text{ite}(P, b, 1)$.
ite_one_mul theorem
{P : Prop} [Decidable P] {a b : M} : ite P 1 (a * b) = ite P 1 a * ite P 1 b
Full source 
@[to_additive]
theorem ite_one_mul {P : Prop} [Decidable P] {a b : M} :
    ite P 1 (a * b) = ite P 1 a * ite P 1 b := by
  by_cases h : P <;> simp [h]
Conditional Identity Preservation in Monoid Multiplication
Informal description
For any proposition $P$ (with a decision procedure), and any elements $a, b$ in a monoid $M$, the conditional expression $\text{ite}(P, 1, a * b)$ equals the product $\text{ite}(P, 1, a) * \text{ite}(P, 1, b)$.
one_mul_eq_id theorem
: ((1 : M) * ·) = id
Full source 
@[to_additive]
theorem one_mul_eq_id : ((1 : M) * ·) = id :=
  funext one_mul
Left multiplication by identity equals identity function
Informal description
For any monoid $M$ with identity element $1$, the left multiplication by $1$ is equal to the identity function, i.e., $1 \cdot x = x$ for all $x \in M$.
mul_one_eq_id theorem
: (· * (1 : M)) = id
Full source 
@[to_additive]
theorem mul_one_eq_id : (· * (1 : M)) = id :=
  funext mul_one
Right Multiplication by Identity is Identity Function
Informal description
For any element $x$ in a monoid $M$ with identity element $1$, the function that multiplies $x$ by $1$ on the right is equal to the identity function, i.e., $x * 1 = x$ for all $x \in M$.
mul_left_comm theorem
(a b c : G) : a * (b * c) = b * (a * c)
Full source 
@[to_additive]
theorem mul_left_comm (a b c : G) : a * (b * c) = b * (a * c) := by
  rw [← mul_assoc, mul_comm a, mul_assoc]
Left Commutativity of Group Multiplication
Informal description
For any elements $a, b, c$ in a group $G$, the following equality holds: $a \cdot (b \cdot c) = b \cdot (a \cdot c)$.
mul_right_comm theorem
(a b c : G) : a * b * c = a * c * b
Full source 
@[to_additive]
theorem mul_right_comm (a b c : G) : a * b * c = a * c * b := by
  rw [mul_assoc, mul_comm b, mul_assoc]
Right Commutativity of Group Multiplication: $(ab)c = (ac)b$
Informal description
For any elements $a, b, c$ in a group $G$, the following equality holds: $(a \cdot b) \cdot c = (a \cdot c) \cdot b$.
mul_mul_mul_comm theorem
(a b c d : G) : a * b * (c * d) = a * c * (b * d)
Full source 
@[to_additive]
theorem mul_mul_mul_comm (a b c d : G) : a * b * (c * d) = a * c * (b * d) := by
  simp only [mul_left_comm, mul_assoc]
Commutation of Double Products: $(ab)(cd) = (ac)(bd)$
Informal description
For any elements $a, b, c, d$ in a group $G$, the following equality holds: $(a \cdot b) \cdot (c \cdot d) = (a \cdot c) \cdot (b \cdot d)$.
mul_rotate theorem
(a b c : G) : a * b * c = b * c * a
Full source 
@[to_additive]
theorem mul_rotate (a b c : G) : a * b * c = b * c * a := by
  simp only [mul_left_comm, mul_comm]
Cyclic Permutation of Group Multiplication: $(ab)c = (bc)a$
Informal description
For any elements $a, b, c$ in a group $G$, the following equality holds: $(a \cdot b) \cdot c = (b \cdot c) \cdot a$.
mul_rotate' theorem
(a b c : G) : a * (b * c) = b * (c * a)
Full source 
@[to_additive]
theorem mul_rotate' (a b c : G) : a * (b * c) = b * (c * a) := by
  simp only [mul_left_comm, mul_comm]
Rotated Group Multiplication: $a(bc) = b(ca)$
Informal description
For any elements $a, b, c$ in a group $G$, the following equality holds: $a \cdot (b \cdot c) = b \cdot (c \cdot a)$.
pow_boole theorem
(P : Prop) [Decidable P] (a : M) : (a ^ if P then 1 else 0) = if P then a else 1
Full source 
@[to_additive boole_nsmul]
lemma pow_boole (P : Prop) [Decidable P] (a : M) :
    (a ^ if P then 1 else 0) = if P then a else 1 := by simp only [pow_ite, pow_one, pow_zero]
Power of Boolean Condition: $a^{\text{if } P \text{ then } 1 \text{ else } 0} = \text{if } P \text{ then } a \text{ else } 1$
Informal description
For any decidable proposition $P$ and any element $a$ in a monoid $M$, we have: $$ a^{\text{if } P \text{ then } 1 \text{ else } 0} = \text{if } P \text{ then } a \text{ else } 1 $$
pow_mul_pow_sub theorem
(a : M) (h : m ≤ n) : a ^ m * a ^ (n - m) = a ^ n
Full source 
@[to_additive nsmul_add_sub_nsmul]
lemma pow_mul_pow_sub (a : M) (h : m ≤ n) : a ^ m * a ^ (n - m) = a ^ n := by
  rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]
Power decomposition: $a^m \cdot a^{n-m} = a^n$ for $m \leq n$
Informal description
For any element $a$ in a monoid $M$ and natural numbers $m, n$ with $m \leq n$, we have $a^m \cdot a^{n-m} = a^n$.
pow_sub_mul_pow theorem
(a : M) (h : m ≤ n) : a ^ (n - m) * a ^ m = a ^ n
Full source 
@[to_additive sub_nsmul_nsmul_add]
lemma pow_sub_mul_pow (a : M) (h : m ≤ n) : a ^ (n - m) * a ^ m = a ^ n := by
  rw [← pow_add, Nat.sub_add_cancel h]
Power subtraction and multiplication identity: $a^{n-m} \cdot a^m = a^n$
Informal description
For any element $a$ in a monoid $M$ and natural numbers $m \leq n$, we have $a^{n-m} \cdot a^m = a^n$.
mul_pow_sub_one theorem
(hn : n ≠ 0) (a : M) : a * a ^ (n - 1) = a ^ n
Full source 
@[to_additive sub_one_nsmul_add]
lemma mul_pow_sub_one (hn : n ≠ 0) (a : M) : a * a ^ (n - 1) = a ^ n := by
  rw [← pow_succ', Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]
Monoid Power Identity: $a \cdot a^{n-1} = a^n$ for $n \neq 0$
Informal description
For any element $a$ in a monoid $M$ and any nonzero natural number $n$, the product of $a$ and $a^{n-1}$ equals $a^n$, i.e., $a \cdot a^{n-1} = a^n$.
pow_sub_one_mul theorem
(hn : n ≠ 0) (a : M) : a ^ (n - 1) * a = a ^ n
Full source 
@[to_additive add_sub_one_nsmul]
lemma pow_sub_one_mul (hn : n ≠ 0) (a : M) : a ^ (n - 1) * a = a ^ n := by
  rw [← pow_succ, Nat.sub_add_cancel <| Nat.one_le_iff_ne_zero.2 hn]
Power Identity: $a^{n-1} \cdot a = a^n$ for $n \neq 0$
Informal description
For any element $a$ in a monoid $M$ and any nonzero natural number $n$, the product of $a^{n-1}$ and $a$ equals $a^n$, i.e., $a^{n-1} \cdot a = a^n$.
pow_eq_pow_mod theorem
(m : ℕ) (ha : a ^ n = 1) : a ^ m = a ^ (m % n)
Full source 
/-- If `x ^ n = 1`, then `x ^ m` is the same as `x ^ (m % n)` -/
@[to_additive nsmul_eq_mod_nsmul "If `n • x = 0`, then `m • x` is the same as `(m % n) • x`"]
lemma pow_eq_pow_mod (m : ℕ) (ha : a ^ n = 1) : a ^ m = a ^ (m % n) := by
  calc
    a ^ m = a ^ (m % n + n * (m / n)) := by rw [Nat.mod_add_div]
    _ = a ^ (m % n) := by simp [pow_add, pow_mul, ha]
Exponentiation Modulo Periodicity: $a^m = a^{m \bmod n}$ when $a^n = 1$
Informal description
Let $a$ be an element of a monoid such that $a^n = 1$ for some natural number $n$. Then for any natural number $m$, we have $a^m = a^{m \bmod n}$.
pow_mul_pow_eq_one theorem
: ∀ n, a * b = 1 → a ^ n * b ^ n = 1
Full source 
@[to_additive] lemma pow_mul_pow_eq_one : ∀ n, a * b = 1 → a ^ n * b ^ n = 1
  | 0, _ => by simp
  | n + 1, h =>
    calc
      a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n) := by rw [pow_succ, pow_succ']
      _ = a ^ n * (a * b) * b ^ n := by simp only [mul_assoc]
      _ = 1 := by simp [h, pow_mul_pow_eq_one]
Power Product Identity: $a * b = 1 \Rightarrow a^n * b^n = 1$
Informal description
For any natural number $n$ and elements $a, b$ in a monoid $M$ such that $a * b = 1$, it holds that $a^n * b^n = 1$.
mul_left_iterate theorem
(a : M) : ∀ n : ℕ, (a * ·)^[n] = (a ^ n * ·)
Full source 
@[to_additive (attr := simp)]
lemma mul_left_iterate (a : M) : ∀ n : ℕ, (a * ·)^[n] = (a ^ n * ·)
  | 0 =>  by ext; simp
  | n + 1 => by ext; simp [pow_succ, mul_left_iterate]
Iterated Left Multiplication Equals Multiplication by Power
Informal description
For any element $a$ in a monoid $M$ and any natural number $n$, the $n$-th iterate of left multiplication by $a$ is equal to left multiplication by $a^n$. That is, $(a \cdot \_)^{[n]} = (a^n \cdot \_)$.
mul_right_iterate theorem
(a : M) : ∀ n : ℕ, (· * a)^[n] = (· * a ^ n)
Full source 
@[to_additive (attr := simp)]
lemma mul_right_iterate (a : M) : ∀ n : ℕ, (· * a)^[n] = (· * a ^ n)
  | 0 =>  by ext; simp
  | n + 1 => by ext; simp [pow_succ', mul_right_iterate]
Iterated Right Multiplication by $a$ Equals Right Multiplication by $a^n$
Informal description
For any element $a$ in a monoid $M$ and any natural number $n$, the $n$-th iterate of the right multiplication function by $a$ is equal to the right multiplication function by $a^n$. In other words, $(x \mapsto x * a)^{[n]} = (x \mapsto x * a^n)$.
mul_left_iterate_apply_one theorem
(a : M) : (a * ·)^[n] 1 = a ^ n
Full source 
@[to_additive]
lemma mul_left_iterate_apply_one (a : M) : (a * ·)^[n] 1 = a ^ n := by simp [mul_right_iterate]
Iterated Left Multiplication at Identity Yields Power: $(a \cdot \_)^{[n]}(1) = a^n$
Informal description
For any element $a$ in a monoid $M$ and any natural number $n$, the $n$-th iterate of the left multiplication function by $a$ applied to the multiplicative identity $1$ equals $a^n$, i.e., $(a \cdot \_)^{[n]}(1) = a^n$.
mul_right_iterate_apply_one theorem
(a : M) : (· * a)^[n] 1 = a ^ n
Full source 
@[to_additive]
lemma mul_right_iterate_apply_one (a : M) : (· * a)^[n] 1 = a ^ n := by simp [mul_right_iterate]
Iterated Right Multiplication at Identity: $(x \mapsto x * a)^{[n]}(1) = a^n$
Informal description
For any element $a$ in a monoid $M$ and any natural number $n$, the $n$-th iterate of the right multiplication function by $a$ evaluated at the identity element $1$ equals $a^n$, i.e., $(x \mapsto x * a)^{[n]}(1) = a^n$.
pow_iterate theorem
(k : ℕ) : ∀ n : ℕ, (fun x : M ↦ x ^ k)^[n] = (· ^ k ^ n)
Full source 
@[to_additive (attr := simp)]
lemma pow_iterate (k : ℕ) : ∀ n : ℕ, (fun x : M ↦ x ^ k)^[n] = (· ^ k ^ n)
  | 0 => by ext; simp
  | n + 1 => by ext; simp [pow_iterate, Nat.pow_succ', pow_mul]
Iterated Power Function Equals Power of Power
Informal description
For any natural number $k$ and any monoid element $x$ in a monoid $M$, the $n$-th iterate of the function $x \mapsto x^k$ is equal to the function $x \mapsto x^{k^n}$.
inv_unique theorem
(hy : x * y = 1) (hz : x * z = 1) : y = z
Full source 
@[to_additive]
theorem inv_unique (hy : x * y = 1) (hz : x * z = 1) : y = z :=
  left_inv_eq_right_inv (Trans.trans (mul_comm _ _) hy) hz
Uniqueness of Right Inverse in a Group
Informal description
For any elements $x, y, z$ in a group, if $x * y = 1$ and $x * z = 1$, then $y = z$.
mul_pow theorem
(a b : M) : ∀ n, (a * b) ^ n = a ^ n * b ^ n
Full source 
@[to_additive nsmul_add] lemma mul_pow (a b : M) : ∀ n, (a * b) ^ n = a ^ n * b ^ n
  | 0 => by rw [pow_zero, pow_zero, pow_zero, one_mul]
  | n + 1 => by rw [pow_succ', pow_succ', pow_succ', mul_pow, mul_mul_mul_comm]
Power of Product Equals Product of Powers: $(ab)^n = a^n b^n$
Informal description
For any elements $a$ and $b$ in a monoid $M$ and any natural number $n$, the $n$-th power of the product $a \cdot b$ is equal to the product of the $n$-th powers of $a$ and $b$, i.e., $(a \cdot b)^n = a^n \cdot b^n$.
left_eq_mul theorem
: a = a * b ↔ b = 1
Full source 
@[to_additive (attr := simp)]
theorem left_eq_mul : a = a * b ↔ b = 1 :=
  eq_comm.trans mul_eq_left
Left Equality with Product if and only if Right Factor is Identity
Informal description
For elements $a$ and $b$ in a monoid, the equality $a = a \cdot b$ holds if and only if $b$ is the identity element, i.e., $a = a \cdot b \leftrightarrow b = 1$.
mul_ne_left theorem
: a * b ≠ a ↔ b ≠ 1
Full source 
@[to_additive]
theorem mul_ne_left : a * b ≠ aa * b ≠ a ↔ b ≠ 1 := mul_eq_left.not
Product Not Equal to Left Factor if and only if Right Factor is Not Identity
Informal description
For elements $a$ and $b$ in a monoid, the product $a \cdot b$ is not equal to $a$ if and only if $b$ is not the identity element, i.e., $a \cdot b \neq a \leftrightarrow b \neq 1$.
left_ne_mul theorem
: a ≠ a * b ↔ b ≠ 1
Full source 
@[to_additive]
theorem left_ne_mul : a ≠ a * ba ≠ a * b ↔ b ≠ 1 := left_eq_mul.not
Inequality with Left Factor if and only if Right Factor is Not Identity
Informal description
For elements $a$ and $b$ in a monoid, the inequality $a \neq a \cdot b$ holds if and only if $b$ is not the identity element, i.e., $a \neq a \cdot b \leftrightarrow b \neq 1$.
right_eq_mul theorem
: b = a * b ↔ a = 1
Full source 
@[to_additive (attr := simp)]
theorem right_eq_mul : b = a * b ↔ a = 1 :=
  eq_comm.trans mul_eq_right
Right Identity Condition: $b = a \cdot b \leftrightarrow a = 1$
Informal description
For elements $a$ and $b$ in a group (or monoid), the equation $b = a \cdot b$ holds if and only if $a$ is the identity element $1$.
mul_ne_right theorem
: a * b ≠ b ↔ a ≠ 1
Full source 
@[to_additive]
theorem mul_ne_right : a * b ≠ ba * b ≠ b ↔ a ≠ 1 := mul_eq_right.not
Right Multiplication by Non-Identity: $a \cdot b \neq b \leftrightarrow a \neq 1$
Informal description
For elements $a$ and $b$ in a group (or monoid), the inequality $a \cdot b \neq b$ holds if and only if $a$ is not the identity element $1$.
right_ne_mul theorem
: b ≠ a * b ↔ a ≠ 1
Full source 
@[to_additive]
theorem right_ne_mul : b ≠ a * bb ≠ a * b ↔ a ≠ 1 := right_eq_mul.not
Inequality Condition for Right Multiplication: $b \neq a \cdot b \leftrightarrow a \neq 1$
Informal description
For elements $a$ and $b$ in a group (or monoid), the inequality $b \neq a \cdot b$ holds if and only if $a$ is not the identity element $1$.
ne_iff_ne_of_mul_eq_mul theorem
(h : a * b = c * d) : a ≠ c ↔ b ≠ d
Full source 
@[to_additive] lemma ne_iff_ne_of_mul_eq_mul (h : a * b = c * d) : a ≠ ca ≠ c ↔ b ≠ d := by aesop
Inequality Preservation under Equal Products: $a \neq c \leftrightarrow b \neq d$ when $a \cdot b = c \cdot d$
Informal description
For elements $a, b, c, d$ in a group (or monoid), if $a \cdot b = c \cdot d$, then $a \neq c$ if and only if $b \neq d$.
inv_involutive theorem
: Function.Involutive (Inv.inv : G → G)
Full source 
@[to_additive (attr := simp)]
theorem inv_involutive : Function.Involutive (Inv.inv : G → G) :=
  inv_inv
Inversion is Involutive in a Group
Informal description
The inversion operation $x \mapsto x^{-1}$ on a group $G$ is involutive, meaning that for every element $x \in G$, $(x^{-1})^{-1} = x$.
inv_surjective theorem
: Function.Surjective (Inv.inv : G → G)
Full source 
@[to_additive (attr := simp)]
theorem inv_surjective : Function.Surjective (Inv.inv : G → G) :=
  inv_involutive.surjective
Inversion is Surjective in a Group
Informal description
The inversion operation $x \mapsto x^{-1}$ on a group $G$ is surjective, meaning that for every element $y \in G$, there exists an element $x \in G$ such that $x^{-1} = y$.
inv_injective theorem
: Function.Injective (Inv.inv : G → G)
Full source 
@[to_additive]
theorem inv_injective : Function.Injective (Inv.inv : G → G) :=
  inv_involutive.injective
Inversion is Injective in a Group
Informal description
The inversion operation $x \mapsto x^{-1}$ on a group $G$ is injective, meaning that for any elements $x, y \in G$, if $x^{-1} = y^{-1}$, then $x = y$.
inv_inj theorem
: a⁻¹ = b⁻¹ ↔ a = b
Full source 
@[to_additive (attr := simp)]
theorem inv_inj : a⁻¹a⁻¹ = b⁻¹ ↔ a = b :=
  inv_injective.eq_iff
Inverse Equality: $a^{-1} = b^{-1} \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ in a group $G$, the inverse of $a$ equals the inverse of $b$ if and only if $a$ equals $b$, i.e., $a^{-1} = b^{-1} \leftrightarrow a = b$.
inv_comp_inv theorem
: Inv.inv ∘ Inv.inv = @id G
Full source 
@[to_additive]
theorem inv_comp_inv : Inv.invInv.inv ∘ Inv.inv = @id G :=
  inv_involutive.comp_self
Double Inversion Yields Identity in Groups
Informal description
The composition of the inversion operation with itself is equal to the identity function on a group $G$, i.e., $x \mapsto (x^{-1})^{-1} = x$ for all $x \in G$.
leftInverse_inv theorem
: LeftInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹
Full source 
@[to_additive]
theorem leftInverse_inv : LeftInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹ :=
  inv_inv
Double Inverse Property in Groups
Informal description
For any element $a$ in a group $G$, the inverse operation is a left inverse of itself, i.e., $(a^{-1})^{-1} = a$.
rightInverse_inv theorem
: RightInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹
Full source 
@[to_additive]
theorem rightInverse_inv : RightInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹ :=
  inv_inv
Double Inverse Property in Groups
Informal description
For any element $a$ in a group $G$, the inverse operation is a right inverse of itself, i.e., $(a^{-1})^{-1} = a$.
mul_one_div theorem
(x y : G) : x * (1 / y) = x / y
Full source 
@[to_additive]
theorem mul_one_div (x y : G) : x * (1 / y) = x / y := by
  rw [div_eq_mul_inv, one_mul, div_eq_mul_inv]
Product with One Over Element Equals Division: $x \cdot (1/y) = x/y$
Informal description
For any elements $x$ and $y$ in a group $G$, the product $x \cdot (1 / y)$ equals $x / y$.
mul_div_assoc' theorem
(a b c : G) : a * (b / c) = a * b / c
Full source 
@[to_additive, field_simps] -- The attributes are out of order on purpose
theorem mul_div_assoc' (a b c : G) : a * (b / c) = a * b / c :=
  (mul_div_assoc _ _ _).symm
Associativity of multiplication and division in a group: $a \cdot (b / c) = (a \cdot b) / c$
Informal description
For any elements $a, b, c$ in a group $G$, the following equality holds: $$a \cdot (b / c) = (a \cdot b) / c$$ where $\cdot$ denotes the group operation and $/$ denotes division in the group (i.e., $x/y = x \cdot y^{-1}$).
mul_div theorem
(a b c : G) : a * (b / c) = a * b / c
Full source 
@[to_additive]
theorem mul_div (a b c : G) : a * (b / c) = a * b / c := by simp only [mul_assoc, div_eq_mul_inv]
Multiplication and Division Interaction in Groups: $a \cdot (b / c) = (a \cdot b) / c$
Informal description
For any elements $a$, $b$, and $c$ in a group $G$, the product of $a$ and the quotient $b/c$ is equal to the quotient of the product $a * b$ and $c$, i.e., $a \cdot (b / c) = (a \cdot b) / c$.
div_eq_mul_one_div theorem
(a b : G) : a / b = a * (1 / b)
Full source 
@[to_additive]
theorem div_eq_mul_one_div (a b : G) : a / b = a * (1 / b) := by rw [div_eq_mul_inv, one_div]
Division as Multiplication by Inverse: $a / b = a \cdot (1 / b)$
Informal description
For any elements $a$ and $b$ in a group $G$, the quotient $a / b$ is equal to the product $a \cdot (1 / b)$.
div_one theorem
(a : G) : a / 1 = a
Full source 
@[to_additive (attr := simp)]
theorem div_one (a : G) : a / 1 = a := by simp [div_eq_mul_inv]
Division by Identity: $a / 1 = a$
Informal description
For any element $a$ in a group $G$, the division of $a$ by the identity element $1$ equals $a$, i.e., $a / 1 = a$.
one_div_one theorem
: (1 : G) / 1 = 1
Full source 
@[to_additive]
theorem one_div_one : (1 : G) / 1 = 1 :=
  div_one _
Identity Division Identity: $1 / 1 = 1$
Informal description
In any group $G$, the division of the identity element $1$ by itself equals $1$, i.e., $1 / 1 = 1$.
div_ne_one_of_ne theorem
: a ≠ b → a / b ≠ 1
Full source 
@[to_additive]
theorem div_ne_one_of_ne : a ≠ b → a / b ≠ 1 :=
  mt eq_of_div_eq_one
Division of distinct elements is not one: $a \neq b \Rightarrow a/b \neq 1$
Informal description
For any elements $a$ and $b$ in a group, if $a \neq b$, then $a / b \neq 1$.
one_div_mul_one_div_rev theorem
: 1 / a * (1 / b) = 1 / (b * a)
Full source 
@[to_additive]
theorem one_div_mul_one_div_rev : 1 / a * (1 / b) = 1 / (b * a) := by simp
Reciprocal Product Identity: $(1/a)(1/b) = 1/(ba)$
Informal description
For any elements $a$ and $b$ in a division monoid, the product of the reciprocals $1/a$ and $1/b$ equals the reciprocal of the product $b * a$, i.e., $(1/a) * (1/b) = 1/(b * a)$.
inv_div_left theorem
: a⁻¹ / b = (b * a)⁻¹
Full source 
@[to_additive]
theorem inv_div_left : a⁻¹ / b = (b * a)⁻¹ := by simp
Inverse-Division Identity: $a^{-1}/b = (b * a)^{-1}$
Informal description
For any elements $a$ and $b$ in a division monoid, the quotient of the inverse of $a$ by $b$ equals the inverse of the product $b * a$, i.e., $a^{-1} / b = (b * a)^{-1}$.
inv_div theorem
: (a / b)⁻¹ = b / a
Full source 
@[to_additive (attr := simp)]
theorem inv_div : (a / b)⁻¹ = b / a := by simp
Inverse of Quotient Equals Reverse Quotient
Informal description
For any elements $a$ and $b$ in a division monoid, the inverse of the quotient $a / b$ equals the quotient $b / a$, i.e., $(a / b)^{-1} = b / a$.
one_div_div theorem
: 1 / (a / b) = b / a
Full source 
@[to_additive]
theorem one_div_div : 1 / (a / b) = b / a := by simp
Reciprocal of Quotient Equals Reverse Quotient
Informal description
For any elements $a$ and $b$ in a division monoid, the reciprocal of the quotient $a / b$ equals the quotient $b / a$, i.e., $\frac{1}{a / b} = \frac{b}{a}$.
one_div_one_div theorem
: 1 / (1 / a) = a
Full source 
@[to_additive]
theorem one_div_one_div : 1 / (1 / a) = a := by simp
Double Reciprocal Identity: $\frac{1}{\frac{1}{a}} = a$
Informal description
For any element $a$ in a division monoid, the reciprocal of the reciprocal of $a$ is equal to $a$ itself, i.e., $\frac{1}{\frac{1}{a}} = a$.
inv_pow theorem
(a : α) : ∀ n : ℕ, a⁻¹ ^ n = (a ^ n)⁻¹
Full source 
@[to_additive (attr := simp)]
lemma inv_pow (a : α) : ∀ n : ℕ, a⁻¹ ^ n = (a ^ n)⁻¹
  | 0 => by rw [pow_zero, pow_zero, inv_one]
  | n + 1 => by rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]
Inverse of Power Equals Power of Inverse
Informal description
For any element $a$ in a group $\alpha$ and any natural number $n$, the $n$-th power of the inverse of $a$ is equal to the inverse of the $n$-th power of $a$, i.e., $(a^{-1})^n = (a^n)^{-1}$.
one_zpow theorem
: ∀ n : ℤ, (1 : α) ^ n = 1
Full source 
@[to_additive zsmul_zero, simp]
lemma one_zpow : ∀ n : ℤ, (1 : α) ^ n = 1
  | (n : ℕ)    => by rw [zpow_natCast, one_pow]
  | .negSucc n => by rw [zpow_negSucc, one_pow, inv_one]
Identity Element to Integer Power Equals Identity: $1^n = 1$
Informal description
For any integer $n$, the $n$-th power of the multiplicative identity element $1$ in a group $\alpha$ is equal to $1$.
zpow_neg theorem
(a : α) : ∀ n : ℤ, a ^ (-n) = (a ^ n)⁻¹
Full source 
@[to_additive (attr := simp) neg_zsmul]
lemma zpow_neg (a : α) : ∀ n : ℤ, a ^ (-n) = (a ^ n)⁻¹
  | (_ + 1 : ℕ) => DivInvMonoid.zpow_neg' _ _
  | 0 => by simp
  | Int.negSucc n => by
    rw [zpow_negSucc, inv_inv, ← zpow_natCast]
    rfl
Negative Integer Power Equals Inverse of Positive Power: $a^{-n} = (a^n)^{-1}$
Informal description
For any element $a$ in a division monoid $\alpha$ and any integer $n$, the $(-n)$-th power of $a$ is equal to the inverse of the $n$-th power of $a$, i.e., $a^{-n} = (a^n)^{-1}$.
mul_zpow_neg_one theorem
(a b : α) : (a * b) ^ (-1 : ℤ) = b ^ (-1 : ℤ) * a ^ (-1 : ℤ)
Full source 
@[to_additive neg_one_zsmul_add]
lemma mul_zpow_neg_one (a b : α) : (a * b) ^ (-1 : ℤ) = b ^ (-1 : ℤ) * a ^ (-1 : ℤ) := by
  simp only [zpow_neg, zpow_one, mul_inv_rev]
Inverse of Product Equals Reverse Product of Inverses: $(ab)^{-1} = b^{-1}a^{-1}$
Informal description
For any elements $a$ and $b$ in a division monoid $\alpha$, the $(-1)$-th power of their product equals the product of the $(-1)$-th powers in reverse order, i.e., $(a \cdot b)^{-1} = b^{-1} \cdot a^{-1}$.
inv_zpow theorem
(a : α) : ∀ n : ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
Full source 
@[to_additive zsmul_neg]
lemma inv_zpow (a : α) : ∀ n : ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
  | (n : ℕ)    => by rw [zpow_natCast, zpow_natCast, inv_pow]
  | .negSucc n => by rw [zpow_negSucc, zpow_negSucc, inv_pow]
Inverse of Integer Power Equals Power of Inverse: $(a^{-1})^n = (a^n)^{-1}$
Informal description
For any element $a$ in a division monoid $\alpha$ and any integer $n$, the $n$-th power of the inverse of $a$ is equal to the inverse of the $n$-th power of $a$, i.e., $(a^{-1})^n = (a^n)^{-1}$.
inv_zpow' theorem
(a : α) (n : ℤ) : a⁻¹ ^ n = a ^ (-n)
Full source 
@[to_additive (attr := simp) zsmul_neg']
lemma inv_zpow' (a : α) (n : ℤ) : a⁻¹ ^ n = a ^ (-n) := by rw [inv_zpow, zpow_neg]
Power of Inverse Equals Negative Power: $(a^{-1})^n = a^{-n}$
Informal description
For any element $a$ in a division monoid $\alpha$ and any integer $n$, the $n$-th power of the inverse of $a$ is equal to the $(-n)$-th power of $a$, i.e., $(a^{-1})^n = a^{-n}$.
one_div_pow theorem
(a : α) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n
Full source 
@[to_additive nsmul_zero_sub]
lemma one_div_pow (a : α) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n := by simp only [one_div, inv_pow]
Power of Reciprocal Equals Reciprocal of Power
Informal description
For any element $a$ in a division monoid $\alpha$ and any natural number $n$, the $n$-th power of the reciprocal of $a$ is equal to the reciprocal of the $n$-th power of $a$, i.e., $(1 / a)^n = 1 / a^n$.
one_div_zpow theorem
(a : α) (n : ℤ) : (1 / a) ^ n = 1 / a ^ n
Full source 
@[to_additive zsmul_zero_sub]
lemma one_div_zpow (a : α) (n : ℤ) : (1 / a) ^ n = 1 / a ^ n := by simp only [one_div, inv_zpow]
Power of Reciprocal Equals Reciprocal of Power: $(1/a)^n = 1/a^n$
Informal description
For any element $a$ in a division monoid $\alpha$ and any integer $n$, the $n$-th power of the reciprocal of $a$ is equal to the reciprocal of the $n$-th power of $a$, i.e., $(1 / a)^n = 1 / a^n$.
inv_eq_one theorem
: a⁻¹ = 1 ↔ a = 1
Full source 
@[to_additive (attr := simp)]
theorem inv_eq_one : a⁻¹a⁻¹ = 1 ↔ a = 1 :=
  inv_injective.eq_iff' inv_one
Inverse Equals Identity if and only if Element Equals Identity
Informal description
For any element $a$ in a group, the inverse of $a$ equals the identity element if and only if $a$ itself equals the identity element, i.e., $a^{-1} = 1 \leftrightarrow a = 1$.
one_eq_inv theorem
: 1 = a⁻¹ ↔ a = 1
Full source 
@[to_additive (attr := simp)]
theorem one_eq_inv : 1 = a⁻¹ ↔ a = 1 :=
  eq_comm.trans inv_eq_one
Identity Equals Inverse if and only if Element Equals Identity
Informal description
For any element $a$ in a group, the identity element equals the inverse of $a$ if and only if $a$ equals the identity element, i.e., $1 = a^{-1} \leftrightarrow a = 1$.
inv_ne_one theorem
: a⁻¹ ≠ 1 ↔ a ≠ 1
Full source 
@[to_additive]
theorem inv_ne_one : a⁻¹a⁻¹ ≠ 1a⁻¹ ≠ 1 ↔ a ≠ 1 :=
  inv_eq_one.not
Inverse Not Equal to Identity if and only if Element Not Equal to Identity
Informal description
For any element $a$ in a group, the inverse of $a$ is not equal to the identity element if and only if $a$ itself is not equal to the identity element, i.e., $a^{-1} \neq 1 \leftrightarrow a \neq 1$.
zpow_mul theorem
(a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
Full source 
@[to_additive mul_zsmul'] lemma zpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
  | (m : ℕ), (n : ℕ) => by
    rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast]
    rfl
  | (m : ℕ), .negSucc n => by
    rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
      ← zpow_natCast]
  | .negSucc m, (n : ℕ) => by
    rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]
  | .negSucc m, .negSucc n => by
    rw [zpow_negSucc, zpow_negSucc, Int.negSucc_mul_negSucc, inv_pow, inv_inv, ← pow_mul, ←
      zpow_natCast]
    rfl
Power of Product Equals Iterated Power: $a^{m \cdot n} = (a^m)^n$
Informal description
For any element $a$ in a division monoid $\alpha$ and any integers $m$ and $n$, the $(m \cdot n)$-th power of $a$ is equal to the $n$-th power of the $m$-th power of $a$, i.e., $a^{m \cdot n} = (a^m)^n$.
zpow_mul' theorem
(a : α) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m
Full source 
@[to_additive mul_zsmul]
lemma zpow_mul' (a : α) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m := by rw [Int.mul_comm, zpow_mul]
Power of Product Equals Iterated Power (Symmetric Form): $a^{m \cdot n} = (a^n)^m$
Informal description
For any element $a$ in a division monoid $\alpha$ and any integers $m$ and $n$, the $(m \cdot n)$-th power of $a$ is equal to the $m$-th power of the $n$-th power of $a$, i.e., $a^{m \cdot n} = (a^n)^m$.
zpow_comm theorem
(a : α) (m n : ℤ) : (a ^ m) ^ n = (a ^ n) ^ m
Full source 
@[to_additive]
theorem zpow_comm (a : α) (m n : ℤ) : (a ^ m) ^ n = (a ^ n) ^ m := by rw [← zpow_mul, zpow_mul']
Commutativity of Iterated Powers: $(a^m)^n = (a^n)^m$
Informal description
For any element $a$ in a division monoid $\alpha$ and any integers $m$ and $n$, the $n$-th power of the $m$-th power of $a$ is equal to the $m$-th power of the $n$-th power of $a$, i.e., $(a^m)^n = (a^n)^m$.
div_div_eq_mul_div theorem
: a / (b / c) = a * c / b
Full source 
@[to_additive, field_simps] -- The attributes are out of order on purpose
theorem div_div_eq_mul_div : a / (b / c) = a * c / b := by simp
Division identity: $a/(b/c) = (a \cdot c)/b$
Informal description
For any elements $a$, $b$, $c$ in a group, the following equality holds: $$ a / (b / c) = (a \cdot c) / b $$
div_inv_eq_mul theorem
: a / b⁻¹ = a * b
Full source 
@[to_additive (attr := simp)]
theorem div_inv_eq_mul : a / b⁻¹ = a * b := by simp
Division by Inverse Equals Multiplication: $a / b^{-1} = a \cdot b$
Informal description
For any elements $a$ and $b$ in a group, the division of $a$ by the inverse of $b$ is equal to the product of $a$ and $b$, i.e., $a / b^{-1} = a \cdot b$.
div_mul_eq_div_div_swap theorem
: a / (b * c) = a / c / b
Full source 
@[to_additive]
theorem div_mul_eq_div_div_swap : a / (b * c) = a / c / b := by
  simp only [mul_assoc, mul_inv_rev, div_eq_mul_inv]
Division over Product Equals Iterated Division: $a / (b \cdot c) = (a / c) / b$
Informal description
For any elements $a$, $b$, and $c$ in a group, the division $a / (b \cdot c)$ is equal to $(a / c) / b$.
mul_inv theorem
: (a * b)⁻¹ = a⁻¹ * b⁻¹
Full source 
@[to_additive neg_add]
theorem mul_inv : (a * b)⁻¹ = a⁻¹ * b⁻¹ := by simp
Inverse of Product Equals Product of Inverses: $(ab)^{-1} = a^{-1}b^{-1}$
Informal description
For any elements $a$ and $b$ in a group, the inverse of their product is equal to the product of their inverses in reverse order, i.e., $(a \cdot b)^{-1} = a^{-1} \cdot b^{-1}$.
inv_div' theorem
: (a / b)⁻¹ = a⁻¹ / b⁻¹
Full source 
@[to_additive]
theorem inv_div' : (a / b)⁻¹ = a⁻¹ / b⁻¹ := by simp
Inverse of Quotient Equals Quotient of Inverses: $(a / b)^{-1} = a^{-1} / b^{-1}$
Informal description
For any elements $a$ and $b$ in a group, the inverse of the quotient $a / b$ is equal to the quotient of the inverses $a^{-1} / b^{-1}$, i.e., $(a / b)^{-1} = a^{-1} / b^{-1}$.
div_eq_inv_mul theorem
: a / b = b⁻¹ * a
Full source 
@[to_additive]
theorem div_eq_inv_mul : a / b = b⁻¹ * a := by simp
Quotient as Inverse Product: $a / b = b^{-1} * a$
Informal description
For any elements $a$ and $b$ in a division monoid $\alpha$, the quotient $a / b$ equals the product of the inverse of $b$ with $a$, i.e., $a / b = b^{-1} * a$.
inv_mul_eq_div theorem
: a⁻¹ * b = b / a
Full source 
@[to_additive]
theorem inv_mul_eq_div : a⁻¹ * b = b / a := by simp
Inverse Product Equals Division: $a^{-1} \cdot b = b / a$
Informal description
For any elements $a$ and $b$ in a division monoid $\alpha$, the product of the inverse of $a$ with $b$ is equal to the division of $b$ by $a$, i.e., $a^{-1} \cdot b = b / a$.
inv_div_comm theorem
(a b : α) : a⁻¹ / b = b⁻¹ / a
Full source 
@[to_additive] lemma inv_div_comm (a b : α) : a⁻¹ / b = b⁻¹ / a := by simp
Inverse-Division Commutativity: $a^{-1}/b = b^{-1}/a$
Informal description
For any elements $a$ and $b$ in a division monoid $\alpha$, the following identity holds: $a^{-1} / b = b^{-1} / a$.
inv_mul' theorem
: (a * b)⁻¹ = a⁻¹ / b
Full source 
@[to_additive]
theorem inv_mul' : (a * b)⁻¹ = a⁻¹ / b := by simp
Inverse of Product Equals Inverse Divided by Second Factor
Informal description
For any elements $a$ and $b$ in a division monoid $\alpha$, the inverse of their product equals the inverse of $a$ divided by $b$, i.e., $(a \cdot b)^{-1} = a^{-1} / b$.
inv_div_inv theorem
: a⁻¹ / b⁻¹ = b / a
Full source 
@[to_additive]
theorem inv_div_inv : a⁻¹ / b⁻¹ = b / a := by simp
Inverse Quotient Identity: $a^{-1} / b^{-1} = b / a$
Informal description
For any elements $a$ and $b$ in a division monoid $\alpha$, the quotient of their inverses equals the quotient of the original elements in reverse order, i.e., $a^{-1} / b^{-1} = b / a$.
inv_inv_div_inv theorem
: (a⁻¹ / b⁻¹)⁻¹ = a / b
Full source 
@[to_additive]
theorem inv_inv_div_inv : (a⁻¹ / b⁻¹)⁻¹ = a / b := by simp
Inverse of Quotient of Inverses Equals Quotient: $(a^{-1} / b^{-1})^{-1} = a / b$
Informal description
For any elements $a$ and $b$ in a division monoid, the inverse of the quotient of their inverses equals the quotient of the original elements, i.e., $(a^{-1} / b^{-1})^{-1} = a / b$.
one_div_mul_one_div theorem
: 1 / a * (1 / b) = 1 / (a * b)
Full source 
@[to_additive]
theorem one_div_mul_one_div : 1 / a * (1 / b) = 1 / (a * b) := by simp
Inverse Product Identity: $\frac{1}{a} \cdot \frac{1}{b} = \frac{1}{a \cdot b}$
Informal description
For any elements $a$ and $b$ in a group, the product of the inverses of $a$ and $b$ equals the inverse of their product, i.e., $\frac{1}{a} \cdot \frac{1}{b} = \frac{1}{a \cdot b}$.
div_right_comm theorem
: a / b / c = a / c / b
Full source 
@[to_additive]
theorem div_right_comm : a / b / c = a / c / b := by simp
Right Commutativity of Division: $a / b / c = a / c / b$
Informal description
For any elements $a$, $b$, and $c$ in a group, the double division $a / b / c$ is equal to $a / c / b$.
div_div theorem
: a / b / c = a / (b * c)
Full source 
@[to_additive, field_simps]
theorem div_div : a / b / c = a / (b * c) := by simp
Double Division Equals Division by Product: $a / b / c = a / (b \cdot c)$
Informal description
For any elements $a$, $b$, and $c$ in a group, the double division $a / b / c$ is equal to $a / (b \cdot c)$.
div_mul theorem
: a / b * c = a / (b / c)
Full source 
@[to_additive]
theorem div_mul : a / b * c = a / (b / c) := by simp
Division-Multiplication Identity: $(a / b) \cdot c = a / (b / c)$
Informal description
For any elements $a$, $b$, and $c$ in a group, the following equality holds: $(a / b) \cdot c = a / (b / c)$.
mul_div_left_comm theorem
: a * (b / c) = b * (a / c)
Full source 
@[to_additive]
theorem mul_div_left_comm : a * (b / c) = b * (a / c) := by simp
Left Commutativity of Multiplication over Division: $a \cdot (b / c) = b \cdot (a / c)$
Informal description
For any elements $a, b, c$ in a group, the following equality holds: $a \cdot (b / c) = b \cdot (a / c)$.
mul_div_right_comm theorem
: a * b / c = a / c * b
Full source 
@[to_additive]
theorem mul_div_right_comm : a * b / c = a / c * b := by simp
Right Commutativity of Division and Multiplication: $\frac{a \cdot b}{c} = \frac{a}{c} \cdot b$
Informal description
For any elements $a, b, c$ in a group, the following equality holds: \[ \frac{a \cdot b}{c} = \frac{a}{c} \cdot b. \]
div_mul_eq_div_div theorem
: a / (b * c) = a / b / c
Full source 
@[to_additive]
theorem div_mul_eq_div_div : a / (b * c) = a / b / c := by simp
Division over Multiplication as Nested Division: $\frac{a}{b \cdot c} = \frac{a / b}{c}$
Informal description
For any elements $a$, $b$, and $c$ in a group, the following equality holds: \[ \frac{a}{b \cdot c} = \frac{a / b}{c}. \]
div_mul_eq_mul_div theorem
: a / b * c = a * c / b
Full source 
@[to_additive, field_simps]
theorem div_mul_eq_mul_div : a / b * c = a * c / b := by simp
Division-Multiplication Commutation: $(a / b) \cdot c = (a \cdot c) / b$
Informal description
For any elements $a$, $b$, and $c$ in a group, the following equality holds: \[ (a / b) \cdot c = (a \cdot c) / b. \]
one_div_mul_eq_div theorem
: 1 / a * b = b / a
Full source 
@[to_additive]
theorem one_div_mul_eq_div : 1 / a * b = b / a := by simp
Inverse-Multiplication Identity: $\frac{1}{a} \cdot b = \frac{b}{a}$
Informal description
For any elements $a$ and $b$ in a group, the product of the inverse of $a$ with $b$ equals the quotient of $b$ by $a$, i.e., \[ \frac{1}{a} \cdot b = \frac{b}{a}. \]
mul_comm_div theorem
: a / b * c = a * (c / b)
Full source 
@[to_additive]
theorem mul_comm_div : a / b * c = a * (c / b) := by simp
Commutative Division-Multiplication Identity: $(a / b) \cdot c = a \cdot (c / b)$
Informal description
For any elements $a$, $b$, and $c$ in a group, the following equality holds: \[ (a / b) \cdot c = a \cdot (c / b). \]
div_mul_comm theorem
: a / b * c = c / b * a
Full source 
@[to_additive]
theorem div_mul_comm : a / b * c = c / b * a := by simp
Commutative Property of Division and Multiplication: $\frac{a}{b} \cdot c = \frac{c}{b} \cdot a$
Informal description
For any elements $a, b, c$ in a group, the following equality holds: \[ \frac{a}{b} \cdot c = \frac{c}{b} \cdot a. \]
div_mul_eq_div_mul_one_div theorem
: a / (b * c) = a / b * (1 / c)
Full source 
@[to_additive]
theorem div_mul_eq_div_mul_one_div : a / (b * c) = a / b * (1 / c) := by simp
Division Identity: $a/(bc) = (a/b)(1/c)$
Informal description
For any elements $a$, $b$, and $c$ in a division monoid, the division operation satisfies the identity: \[ a / (b \cdot c) = (a / b) \cdot (1 / c). \]
div_div_div_eq theorem
: a / b / (c / d) = a * d / (b * c)
Full source 
@[to_additive]
theorem div_div_div_eq : a / b / (c / d) = a * d / (b * c) := by simp
Double Division Identity: $\frac{a/b}{c/d} = \frac{a \cdot d}{b \cdot c}$
Informal description
For any elements $a, b, c, d$ in a group $G$, the following equality holds: \[ \frac{a/b}{c/d} = \frac{a \cdot d}{b \cdot c}. \]
div_div_div_comm theorem
: a / b / (c / d) = a / c / (b / d)
Full source 
@[to_additive]
theorem div_div_div_comm : a / b / (c / d) = a / c / (b / d) := by simp
Division Chain Commutativity: $\frac{a/b}{c/d} = \frac{a/c}{b/d}$
Informal description
For any elements $a, b, c, d$ in a group $G$, the following equality holds: \[ \frac{a / b}{c / d} = \frac{a / c}{b / d}. \]
div_mul_div_comm theorem
: a / b * (c / d) = a * c / (b * d)
Full source 
@[to_additive]
theorem div_mul_div_comm : a / b * (c / d) = a * c / (b * d) := by simp
Commutative Property of Division and Multiplication in Groups: $\frac{a}{b} \cdot \frac{c}{d} = \frac{a \cdot c}{b \cdot d}$
Informal description
For any elements $a, b, c, d$ in a group $G$, the following equality holds: \[ \frac{a}{b} \cdot \frac{c}{d} = \frac{a \cdot c}{b \cdot d}. \]
mul_div_mul_comm theorem
: a * b / (c * d) = a / c * (b / d)
Full source 
@[to_additive]
theorem mul_div_mul_comm : a * b / (c * d) = a / c * (b / d) := by simp
Commutative Property of Multiplication and Division in Groups: $\frac{a \cdot b}{c \cdot d} = \frac{a}{c} \cdot \frac{b}{d}$
Informal description
For any elements $a, b, c, d$ in a group $G$, the following equality holds: \[ \frac{a \cdot b}{c \cdot d} = \frac{a}{c} \cdot \frac{b}{d}. \]
mul_zpow theorem
: ∀ n : ℤ, (a * b) ^ n = a ^ n * b ^ n
Full source 
@[to_additive zsmul_add] lemma mul_zpow : ∀ n : ℤ, (a * b) ^ n = a ^ n * b ^ n
  | (n : ℕ) => by simp_rw [zpow_natCast, mul_pow]
  | .negSucc n => by simp_rw [zpow_negSucc, ← inv_pow, mul_inv, mul_pow]
Power of Product Equals Product of Powers for Integer Exponents: $(ab)^n = a^n b^n$
Informal description
For any elements $a$ and $b$ in a group and any integer $n$, the $n$-th power of the product $a \cdot b$ is equal to the product of the $n$-th powers of $a$ and $b$, i.e., $(a \cdot b)^n = a^n \cdot b^n$.
div_pow theorem
(a b : α) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n
Full source 
@[to_additive nsmul_sub]
lemma div_pow (a b : α) (n : ℕ) : (a / b) ^ n = a ^ n / b ^ n := by
  simp only [div_eq_mul_inv, mul_pow, inv_pow]
Power of Quotient Equals Quotient of Powers: $(a / b)^n = a^n / b^n$
Informal description
For any elements $a$ and $b$ in a group $\alpha$ and any natural number $n$, the $n$-th power of the quotient $a / b$ is equal to the quotient of the $n$-th powers of $a$ and $b$, i.e., $(a / b)^n = a^n / b^n$.
div_zpow theorem
(a b : α) (n : ℤ) : (a / b) ^ n = a ^ n / b ^ n
Full source 
@[to_additive zsmul_sub]
lemma div_zpow (a b : α) (n : ℤ) : (a / b) ^ n = a ^ n / b ^ n := by
  simp only [div_eq_mul_inv, mul_zpow, inv_zpow]
Power of Quotient Equals Quotient of Powers for Integer Exponents: $(a / b)^n = a^n / b^n$
Informal description
For any elements $a$ and $b$ in a division monoid $\alpha$ and any integer $n$, the $n$-th power of the quotient $a / b$ is equal to the quotient of the $n$-th powers of $a$ and $b$, i.e., $(a / b)^n = a^n / b^n$.
mul_right_surjective theorem
(a : G) : Function.Surjective fun x ↦ x * a
Full source 
@[to_additive]
theorem mul_right_surjective (a : G) : Function.Surjective fun x ↦ x * a := fun x ↦
  ⟨x * a⁻¹, inv_mul_cancel_right x a⟩
Right Multiplication by Group Element is Surjective
Informal description
For any element $a$ in a group $G$, the function $x \mapsto x * a$ is surjective. That is, for every $y \in G$, there exists an $x \in G$ such that $x * a = y$.
inv_mul_eq_of_eq_mul theorem
(h : b = a * c) : a⁻¹ * b = c
Full source 
@[to_additive]
theorem inv_mul_eq_of_eq_mul (h : b = a * c) : a⁻¹ * b = c := by simp [h]
Inverse Multiplication Property: $a^{-1} \cdot (a \cdot c) = c$
Informal description
For elements $a$, $b$, and $c$ in a group, if $b = a \cdot c$, then $a^{-1} \cdot b = c$.
mul_inv_eq_of_eq_mul theorem
(h : a = c * b) : a * b⁻¹ = c
Full source 
@[to_additive]
theorem mul_inv_eq_of_eq_mul (h : a = c * b) : a * b⁻¹ = c := by simp [h]
Right Multiplication by Inverse from Right Equation
Informal description
For elements $a, b, c$ in a division monoid, if $a = c * b$, then $a * b^{-1} = c$.
mul_eq_of_eq_inv_mul theorem
(h : b = a⁻¹ * c) : a * b = c
Full source 
@[to_additive]
theorem mul_eq_of_eq_inv_mul (h : b = a⁻¹ * c) : a * b = c := by rw [h, mul_inv_cancel_left]
Multiplication by Inverse Yields Original Element
Informal description
For elements $a, b, c$ in a group, if $b = a^{-1} * c$, then $a * b = c$.
mul_eq_of_eq_mul_inv theorem
(h : a = c * b⁻¹) : a * b = c
Full source 
@[to_additive]
theorem mul_eq_of_eq_mul_inv (h : a = c * b⁻¹) : a * b = c := by simp [h]
Multiplication by Inverse: $a = c \cdot b^{-1}$ implies $a \cdot b = c$
Informal description
Let $a, b, c$ be elements of a division monoid. If $a = c \cdot b^{-1}$, then $a \cdot b = c$.
mul_eq_one_iff_eq_inv' theorem
: a * b = 1 ↔ b = a⁻¹
Full source 
/-- Variant of `mul_eq_one_iff_eq_inv` with swapped equality. -/
@[to_additive]
theorem mul_eq_one_iff_eq_inv' : a * b = 1 ↔ b = a⁻¹ := by
  rw [mul_eq_one_iff_inv_eq, eq_comm]
Product Equals Identity iff Element is Inverse (Symmetric Form)
Informal description
For any elements $a$ and $b$ in a group, the product $a \cdot b$ equals the identity element $1$ if and only if $b$ equals the inverse of $a$, i.e., $a \cdot b = 1 \leftrightarrow b = a^{-1}$.
mul_eq_one_iff_inv_eq' theorem
: a * b = 1 ↔ b⁻¹ = a
Full source 
/-- Variant of `mul_eq_one_iff_inv_eq` with swapped equality. -/
@[to_additive]
theorem mul_eq_one_iff_inv_eq' : a * b = 1 ↔ b⁻¹ = a := by
  rw [mul_eq_one_iff_eq_inv, eq_comm]
Product Equals Identity iff Inverse Equals Element (Symmetric Form)
Informal description
For elements $a$ and $b$ in a group, the product $a \cdot b$ equals the identity element $1$ if and only if the inverse of $b$ equals $a$, i.e., $a \cdot b = 1 \leftrightarrow b^{-1} = a$.
inv_eq_iff_mul_eq_one theorem
: a⁻¹ = b ↔ a * b = 1
Full source 
@[to_additive]
theorem inv_eq_iff_mul_eq_one : a⁻¹a⁻¹ = b ↔ a * b = 1 :=
  mul_eq_one_iff_inv_eq.symm
Inverse Equals Element iff Product Equals Identity
Informal description
For any elements $a$ and $b$ in a group, the inverse of $a$ equals $b$ if and only if the product $a \cdot b$ equals the identity element $1$, i.e., $a^{-1} = b \leftrightarrow a \cdot b = 1$.
mul_inv_eq_iff_eq_mul theorem
: a * b⁻¹ = c ↔ a = c * b
Full source 
@[to_additive]
theorem mul_inv_eq_iff_eq_mul : a * b⁻¹ = c ↔ a = c * b :=
  ⟨fun h ↦ by rw [← h, inv_mul_cancel_right], fun h ↦ by rw [h, mul_inv_cancel_right]⟩
Equivalence of Product with Inverse and Rearranged Product: $a \cdot b^{-1} = c \leftrightarrow a = c \cdot b$
Informal description
For elements $a$, $b$, and $c$ in a division monoid, the equation $a \cdot b^{-1} = c$ holds if and only if $a = c \cdot b$.
inv_mul_eq_one theorem
: a⁻¹ * b = 1 ↔ a = b
Full source 
@[to_additive]
theorem inv_mul_eq_one : a⁻¹a⁻¹ * b = 1 ↔ a = b := by rw [mul_eq_one_iff_eq_inv, inv_inj]
Inverse Product Identity: $a^{-1} \cdot b = 1 \leftrightarrow a = b$
Informal description
For any elements $a$ and $b$ in a division monoid, the product of the inverse of $a$ and $b$ equals the identity element if and only if $a$ equals $b$, i.e., $a^{-1} \cdot b = 1 \leftrightarrow a = b$.
conj_eq_one_iff theorem
: a * b * a⁻¹ = 1 ↔ b = 1
Full source 
@[to_additive (attr := simp)]
theorem conj_eq_one_iff : a * b * a⁻¹ = 1 ↔ b = 1 := by
  rw [mul_inv_eq_one, mul_eq_left]
Conjugate Equals Identity iff Element is Identity: $a \cdot b \cdot a^{-1} = 1 \leftrightarrow b = 1$
Informal description
For elements $a$ and $b$ in a group, the conjugate $a \cdot b \cdot a^{-1}$ equals the identity element $1$ if and only if $b$ equals $1$, i.e., $a \cdot b \cdot a^{-1} = 1 \leftrightarrow b = 1$.
div_left_injective theorem
: Function.Injective fun a ↦ a / b
Full source 
@[to_additive]
theorem div_left_injective : Function.Injective fun a ↦ a / b := by
  -- FIXME this could be by `simpa`, but it fails. This is probably a bug in `simpa`.
  simp only [div_eq_mul_inv]
  exact fun a a' h ↦ mul_left_injective b⁻¹ h
Injectivity of Left Division by a Fixed Element
Informal description
For any element $b$ in a division monoid, the function $a \mapsto a / b$ is injective.
div_right_injective theorem
: Function.Injective fun a ↦ b / a
Full source 
@[to_additive]
theorem div_right_injective : Function.Injective fun a ↦ b / a := by
  -- FIXME see above
  simp only [div_eq_mul_inv]
  exact fun a a' h ↦ inv_injective (mul_right_injective b h)
Injectivity of Right Division by a Fixed Element in a Group
Informal description
For any fixed element $b$ in a group $G$, the function $a \mapsto b / a$ is injective, meaning that if $b / a_1 = b / a_2$ for some $a_1, a_2 \in G$, then $a_1 = a_2$.
div_mul_cancel_right theorem
(a b : G) : a / (b * a) = b⁻¹
Full source 
@[to_additive (attr := simp)]
lemma div_mul_cancel_right (a b : G) : a / (b * a) = b⁻¹ := by rw [← inv_div, mul_div_cancel_right]
Quotient Identity: $a / (b \cdot a) = b^{-1}$
Informal description
For any elements $a$ and $b$ in a group $G$, the quotient $a / (b \cdot a)$ equals the inverse of $b$, i.e., $a / (b \cdot a) = b^{-1}$.
mul_div_mul_right_eq_div theorem
(a b c : G) : a * c / (b * c) = a / b
Full source 
@[to_additive (attr := simp)]
theorem mul_div_mul_right_eq_div (a b c : G) : a * c / (b * c) = a / b := by
  rw [div_mul_eq_div_div_swap]; simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel_right]
Cancellation of Right Multiplication in Division: $(a \cdot c)/(b \cdot c) = a/b$
Informal description
For any elements $a$, $b$, and $c$ in a group $G$, the following equality holds: $$(a \cdot c) / (b \cdot c) = a / b$$
div_eq_of_eq_mul'' theorem
(h : a = c * b) : a / b = c
Full source 
@[to_additive sub_eq_of_eq_add]
theorem div_eq_of_eq_mul'' (h : a = c * b) : a / b = c := by simp [h]
Division by $b$ when $a$ equals $c * b$
Informal description
For elements $a, b, c$ in a group $G$, if $a = c * b$, then $a / b = c$.
mul_eq_of_eq_div theorem
(h : a = c / b) : a * b = c
Full source 
@[to_additive]
theorem mul_eq_of_eq_div (h : a = c / b) : a * b = c := by simp [h]
Multiplication from Division Equality: $a = c / b$ implies $a \cdot b = c$
Informal description
For elements $a$, $b$, and $c$ in a group, if $a = c / b$, then $a \cdot b = c$.
div_right_inj theorem
: a / b = a / c ↔ b = c
Full source 
@[to_additive (attr := simp)]
theorem div_right_inj : a / b = a / c ↔ b = c :=
  div_right_injective.eq_iff
Right Division Cancellation in Groups: $a / b = a / c \leftrightarrow b = c$
Informal description
For any elements $a, b, c$ in a group $G$, the equality $a / b = a / c$ holds if and only if $b = c$.
div_mul_div_cancel theorem
(a b c : G) : a / b * (b / c) = a / c
Full source 
@[to_additive (attr := simp)]
theorem div_mul_div_cancel (a b c : G) : a / b * (b / c) = a / c := by
  rw [← mul_div_assoc, div_mul_cancel]
Group Division-Multiplication Identity: $(a / b) \cdot (b / c) = a / c$
Informal description
For any elements $a, b, c$ in a group $G$, the following identity holds: $(a / b) \cdot (b / c) = a / c$.
div_div_div_cancel_right theorem
(a b c : G) : a / c / (b / c) = a / b
Full source 
@[to_additive (attr := simp)]
theorem div_div_div_cancel_right (a b c : G) : a / c / (b / c) = a / b := by
  rw [← inv_div c b, div_inv_eq_mul, div_mul_div_cancel]
Right Division Cancellation in Groups: $(a / c) / (b / c) = a / b$
Informal description
For any elements $a, b, c$ in a group $G$, the following identity holds: $(a / c) / (b / c) = a / b$.
div_ne_one theorem
: a / b ≠ 1 ↔ a ≠ b
Full source 
@[to_additive]
theorem div_ne_one : a / b ≠ 1a / b ≠ 1 ↔ a ≠ b :=
  not_congr div_eq_one
Quotient Not Equal to Identity iff Elements Not Equal: $a / b \neq 1 \leftrightarrow a \neq b$
Informal description
For any elements $a$ and $b$ in a group, the quotient $a / b$ is not equal to the identity element $1$ if and only if $a$ is not equal to $b$.
div_eq_self theorem
: a / b = a ↔ b = 1
Full source 
@[to_additive (attr := simp)]
theorem div_eq_self : a / b = a ↔ b = 1 := by rw [div_eq_mul_inv, mul_eq_left, inv_eq_one]
Quotient Equals Dividend if and only if Divisor is Identity: $a / b = a \leftrightarrow b = 1$
Informal description
For any elements $a$ and $b$ in a division monoid, the quotient $a / b$ equals $a$ if and only if $b$ is the identity element, i.e., $a / b = a \leftrightarrow b = 1$.
leftInverse_div_mul_left theorem
(c : G) : Function.LeftInverse (fun x ↦ x / c) fun x ↦ x * c
Full source 
@[to_additive]
theorem leftInverse_div_mul_left (c : G) : Function.LeftInverse (fun x ↦ x / c) fun x ↦ x * c :=
  fun x ↦ mul_div_cancel_right x c
Left inverse property of division and multiplication in a group
Informal description
For any element $c$ in a group $G$, the function $x \mapsto x / c$ is a left inverse of the function $x \mapsto x * c$. That is, for all $x \in G$, we have $(x * c) / c = x$.
leftInverse_mul_left_div theorem
(c : G) : Function.LeftInverse (fun x ↦ x * c) fun x ↦ x / c
Full source 
@[to_additive]
theorem leftInverse_mul_left_div (c : G) : Function.LeftInverse (fun x ↦ x * c) fun x ↦ x / c :=
  fun x ↦ div_mul_cancel x c
Left Inverse Property: $(x / c) * c = x$ in Groups
Informal description
For any element $c$ in a group $G$, the function $x \mapsto x * c$ is a left inverse of the function $x \mapsto x / c$. That is, for all $x \in G$, we have $(x / c) * c = x$.
leftInverse_mul_right_inv_mul theorem
(c : G) : Function.LeftInverse (fun x ↦ c * x) fun x ↦ c⁻¹ * x
Full source 
@[to_additive]
theorem leftInverse_mul_right_inv_mul (c : G) :
    Function.LeftInverse (fun x ↦ c * x) fun x ↦ c⁻¹ * x :=
  fun x ↦ mul_inv_cancel_left c x
Left Inverse Property: $c \cdot (c^{-1} \cdot x) = x$ in Groups
Informal description
For any element $c$ in a group $G$, the function $x \mapsto c \cdot x$ is a left inverse of the function $x \mapsto c^{-1} \cdot x$. That is, for all $x \in G$, we have $c \cdot (c^{-1} \cdot x) = x$.
leftInverse_inv_mul_mul_right theorem
(c : G) : Function.LeftInverse (fun x ↦ c⁻¹ * x) fun x ↦ c * x
Full source 
@[to_additive]
theorem leftInverse_inv_mul_mul_right (c : G) :
    Function.LeftInverse (fun x ↦ c⁻¹ * x) fun x ↦ c * x :=
  fun x ↦ inv_mul_cancel_left c x
Left Inverse Property: $c^{-1} * (c * x) = x$ in Groups
Informal description
For any element $c$ in a group $G$, the function $x \mapsto c^{-1} * x$ is a left inverse of the function $x \mapsto c * x$. That is, for all $x \in G$, we have $c^{-1} * (c * x) = x$.
pow_natAbs_eq_one theorem
: a ^ n.natAbs = 1 ↔ a ^ n = 1
Full source 
@[to_additive (attr := simp) natAbs_nsmul_eq_zero]
lemma pow_natAbs_eq_one : a ^ n.natAbs = 1 ↔ a ^ n = 1 := by cases n <;> simp
Power Identity: $a^{|n|} = 1 \leftrightarrow a^n = 1$
Informal description
For any element $a$ in a group and any integer $n$, the element $a$ raised to the absolute value of $n$ equals the identity element if and only if $a$ raised to the power of $n$ equals the identity element. In other words, $a^{|n|} = 1 \leftrightarrow a^n = 1$.
pow_sub theorem
(a : G) {m n : ℕ} (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹
Full source 
@[to_additive sub_nsmul]
lemma pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=
  eq_mul_inv_of_mul_eq <| by rw [← pow_add, Nat.sub_add_cancel h]
Power Subtraction Identity: $a^{m - n} = a^m \cdot (a^n)^{-1}$
Informal description
For any element $a$ in a group $G$ and any natural numbers $m$ and $n$ such that $n \leq m$, we have $a^{m - n} = a^m \cdot (a^n)^{-1}$.
inv_pow_sub theorem
(a : G) {m n : ℕ} (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
Full source 
@[to_additive sub_nsmul_neg]
theorem inv_pow_sub (a : G) {m n : ℕ} (h : n ≤ m) : a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n := by
  rw [pow_sub a⁻¹ h, inv_pow, inv_pow, inv_inv]
Inverse Power Subtraction Identity: $(a^{-1})^{m - n} = (a^m)^{-1} \cdot a^n$
Informal description
For any element $a$ in a group $G$ and any natural numbers $m$ and $n$ such that $n \leq m$, the $(m - n)$-th power of the inverse of $a$ equals the product of the inverse of the $m$-th power of $a$ and the $n$-th power of $a$, i.e., $(a^{-1})^{m - n} = (a^m)^{-1} \cdot a^n$.
zpow_add_one theorem
(a : G) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
Full source 
@[to_additive add_one_zsmul]
lemma zpow_add_one (a : G) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
  | (n : ℕ) => by simp only [← Int.natCast_succ, zpow_natCast, pow_succ]
  | -1 => by simp [Int.add_left_neg]
  | .negSucc (n + 1) => by
    rw [zpow_negSucc, pow_succ', mul_inv_rev, inv_mul_cancel_right]
    rw [Int.negSucc_eq, Int.neg_add, Int.neg_add_cancel_right]
    exact zpow_negSucc _ _
Integer Power Addition Identity: $a^{n+1} = a^n \cdot a$
Informal description
For any element $a$ in a group $G$ and any integer $n$, the $(n+1)$-th power of $a$ equals the product of the $n$-th power of $a$ and $a$ itself, i.e., $a^{n+1} = a^n \cdot a$.
zpow_sub_one theorem
(a : G) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹
Full source 
@[to_additive sub_one_zsmul]
lemma zpow_sub_one (a : G) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
  calc
    a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹ := (mul_inv_cancel_right _ _).symm
    _ = a ^ n * a⁻¹ := by rw [← zpow_add_one, Int.sub_add_cancel]
Integer Power Subtraction Identity: $a^{n-1} = a^n \cdot a^{-1}$
Informal description
For any element $a$ in a group $G$ and any integer $n$, the $(n-1)$-th power of $a$ equals the product of the $n$-th power of $a$ and the inverse of $a$, i.e., $a^{n-1} = a^n \cdot a^{-1}$.
zpow_add theorem
(a : G) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n
Full source 
@[to_additive add_zsmul]
lemma zpow_add (a : G) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by
  induction n with
  | hz => simp
  | hp n ihn => simp only [← Int.add_assoc, zpow_add_one, ihn, mul_assoc]
  | hn n ihn => rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, Int.add_sub_assoc]
Integer Power Addition Law: $a^{m+n} = a^m \cdot a^n$
Informal description
For any element $a$ in a group $G$ and any integers $m$ and $n$, the $(m+n)$-th power of $a$ equals the product of the $m$-th power of $a$ and the $n$-th power of $a$, i.e., $a^{m+n} = a^m \cdot a^n$.
zpow_one_add theorem
(a : G) (n : ℤ) : a ^ (1 + n) = a * a ^ n
Full source 
@[to_additive one_add_zsmul]
lemma zpow_one_add (a : G) (n : ℤ) : a ^ (1 + n) = a * a ^ n := by rw [zpow_add, zpow_one]
Integer Power Identity: $a^{1+n} = a \cdot a^n$
Informal description
For any element $a$ in a group $G$ and any integer $n$, the $(1 + n)$-th power of $a$ equals the product of $a$ and the $n$-th power of $a$, i.e., $a^{1+n} = a \cdot a^n$.
mul_self_zpow theorem
(a : G) (n : ℤ) : a * a ^ n = a ^ (n + 1)
Full source 
@[to_additive add_zsmul_self]
lemma mul_self_zpow (a : G) (n : ℤ) : a * a ^ n = a ^ (n + 1) := by
  rw [Int.add_comm, zpow_add, zpow_one]
Product-Power Identity: $a \cdot a^n = a^{n+1}$
Informal description
For any element $a$ in a group $G$ and any integer $n$, the product of $a$ and the $n$-th power of $a$ equals the $(n+1)$-th power of $a$, i.e., $a \cdot a^n = a^{n+1}$.
mul_zpow_self theorem
(a : G) (n : ℤ) : a ^ n * a = a ^ (n + 1)
Full source 
@[to_additive add_self_zsmul]
lemma mul_zpow_self (a : G) (n : ℤ) : a ^ n * a = a ^ (n + 1) := (zpow_add_one ..).symm
Integer Power Multiplication Identity: $a^n \cdot a = a^{n+1}$
Informal description
For any element $a$ in a group $G$ and any integer $n$, the product of the $n$-th power of $a$ and $a$ itself equals the $(n+1)$-th power of $a$, i.e., $a^n \cdot a = a^{n+1}$.
zpow_sub theorem
(a : G) (m n : ℤ) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹
Full source 
@[to_additive sub_zsmul] lemma zpow_sub (a : G) (m n : ℤ) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ := by
  rw [Int.sub_eq_add_neg, zpow_add, zpow_neg]
Integer Power Subtraction Law: $a^{m-n} = a^m \cdot (a^n)^{-1}$
Informal description
For any element $a$ in a group $G$ and any integers $m$ and $n$, the $(m-n)$-th power of $a$ equals the product of the $m$-th power of $a$ and the inverse of the $n$-th power of $a$, i.e., $a^{m-n} = a^m \cdot (a^n)^{-1}$.
zpow_natCast_sub_natCast theorem
(a : G) (m n : ℕ) : a ^ (m - n : ℤ) = a ^ m / a ^ n
Full source 
@[to_additive natCast_sub_natCast_zsmul]
lemma zpow_natCast_sub_natCast (a : G) (m n : ℕ) : a ^ (m - n : ℤ) = a ^ m / a ^ n := by
  simpa [div_eq_mul_inv] using zpow_sub a m n
Integer Power Difference Formula for Natural Exponents: $a^{m-n} = a^m / a^n$
Informal description
For any element $a$ in a group $G$ and any natural numbers $m$ and $n$, the $(m-n)$-th integer power of $a$ equals the quotient of the $m$-th power of $a$ by the $n$-th power of $a$, i.e., $a^{m-n} = a^m / a^n$.
zpow_natCast_sub_one theorem
(a : G) (n : ℕ) : a ^ (n - 1 : ℤ) = a ^ n / a
Full source 
@[to_additive natCast_sub_one_zsmul]
lemma zpow_natCast_sub_one (a : G) (n : ℕ) : a ^ (n - 1 : ℤ) = a ^ n / a := by
  simpa [div_eq_mul_inv] using zpow_sub a n 1
Integer Power Identity: $a^{n-1} = a^n / a$
Informal description
For any element $a$ in a group $G$ and any natural number $n$, the $(n-1)$-th integer power of $a$ equals the $n$-th power of $a$ divided by $a$, i.e., $a^{n-1} = a^n / a$.
zpow_one_sub_natCast theorem
(a : G) (n : ℕ) : a ^ (1 - n : ℤ) = a / a ^ n
Full source 
@[to_additive one_sub_natCast_zsmul]
lemma zpow_one_sub_natCast (a : G) (n : ℕ) : a ^ (1 - n : ℤ) = a / a ^ n := by
  simpa [div_eq_mul_inv] using zpow_sub a 1 n
Integer Power Identity: $a^{1-n} = a / a^n$
Informal description
For any element $a$ in a group $G$ and any natural number $n$, the $(1-n)$-th power of $a$ (as an integer exponent) equals the quotient of $a$ by the $n$-th power of $a$, i.e., $a^{1-n} = a / a^n$.
zpow_mul_comm theorem
(a : G) (m n : ℤ) : a ^ m * a ^ n = a ^ n * a ^ m
Full source 
@[to_additive] lemma zpow_mul_comm (a : G) (m n : ℤ) : a ^ m * a ^ n = a ^ n * a ^ m := by
  rw [← zpow_add, Int.add_comm, zpow_add]
Commutativity of Integer Powers in Groups: $a^m \cdot a^n = a^n \cdot a^m$
Informal description
For any element $a$ in a group $G$ and any integers $m$ and $n$, the product of the $m$-th power of $a$ and the $n$-th power of $a$ is commutative, i.e., $a^m \cdot a^n = a^n \cdot a^m$.
zpow_eq_zpow_emod theorem
{x : G} (m : ℤ) {n : ℤ} (h : x ^ n = 1) : x ^ m = x ^ (m % n)
Full source 
theorem zpow_eq_zpow_emod {x : G} (m : ℤ) {n : ℤ} (h : x ^ n = 1) :
    x ^ m = x ^ (m % n) :=
  calc
    x ^ m = x ^ (m % n + n * (m / n)) := by rw [Int.emod_add_ediv]
    _ = x ^ (m % n) := by simp [zpow_add, zpow_mul, h]
Integer Power Equivalence Modulo Periodicity: $x^m = x^{m \bmod n}$ when $x^n = 1$
Informal description
For any element $x$ in a group $G$ and any integers $m$ and $n$, if $x^n = 1$, then $x^m = x^{m \bmod n}$.
zpow_eq_zpow_emod' theorem
{x : G} (m : ℤ) {n : ℕ} (h : x ^ n = 1) : x ^ m = x ^ (m % (n : ℤ))
Full source 
theorem zpow_eq_zpow_emod' {x : G} (m : ℤ) {n : ℕ} (h : x ^ n = 1) :
    x ^ m = x ^ (m % (n : ℤ)) := zpow_eq_zpow_emod m (by simpa)
Integer Power Equivalence Modulo Periodicity for Natural Exponents: $x^m = x^{m \bmod n}$ when $x^n = 1$
Informal description
For any element $x$ in a group $G$ and any integer $m$, if $x^n = 1$ for some natural number $n$, then $x^m = x^{m \bmod n}$.
zpow_iterate theorem
(k : ℤ) : ∀ n : ℕ, (fun x : G ↦ x ^ k)^[n] = (· ^ k ^ n)
Full source 
@[to_additive (attr := simp)]
lemma zpow_iterate (k : ℤ) : ∀ n : ℕ, (fun x : G ↦ x ^ k)^[n] = (· ^ k ^ n)
  | 0 => by ext; simp [Int.pow_zero]
  | n + 1 => by ext; simp [zpow_iterate, Int.pow_succ', zpow_mul]
Iterated Power Law: $(x \mapsto x^k)^{\circ n} = (x \mapsto x^{k^n})$
Informal description
For any integer $k$ and natural number $n$, the $n$-th iterate of the function $x \mapsto x^k$ is equal to the function $x \mapsto x^{k^n}$.
zpow_induction_left theorem
{g : G} {P : G → Prop} (h_one : P (1 : G)) (h_mul : ∀ a, P a → P (g * a)) (h_inv : ∀ a, P a → P (g⁻¹ * a)) (n : ℤ) : P (g ^ n)
Full source 
/-- To show a property of all powers of `g` it suffices to show it is closed under multiplication
by `g` and `g⁻¹` on the left. For subgroups generated by more than one element, see
`Subgroup.closure_induction_left`. -/
@[to_additive "To show a property of all multiples of `g` it suffices to show it is closed under
addition by `g` and `-g` on the left. For additive subgroups generated by more than one element, see
`AddSubgroup.closure_induction_left`."]
lemma zpow_induction_left {g : G} {P : G → Prop} (h_one : P (1 : G))
    (h_mul : ∀ a, P a → P (g * a)) (h_inv : ∀ a, P a → P (g⁻¹ * a)) (n : ℤ) : P (g ^ n) := by
  induction n with
  | hz => rwa [zpow_zero]
  | hp n ih =>
    rw [Int.add_comm, zpow_add, zpow_one]
    exact h_mul _ ih
  | hn n ih =>
    rw [Int.sub_eq_add_neg, Int.add_comm, zpow_add, zpow_neg_one]
    exact h_inv _ ih
Left Induction Principle for Integer Powers in Groups
Informal description
Let $G$ be a group and $g \in G$. To prove that a property $P$ holds for all integer powers $g^n$ (for $n \in \mathbb{Z}$), it suffices to show: 1. $P$ holds for the identity element ($P(1)$), 2. For any $a \in G$, if $P(a)$ holds then $P(g \cdot a)$ holds, and 3. For any $a \in G$, if $P(a)$ holds then $P(g^{-1} \cdot a)$ holds.
zpow_induction_right theorem
{g : G} {P : G → Prop} (h_one : P (1 : G)) (h_mul : ∀ a, P a → P (a * g)) (h_inv : ∀ a, P a → P (a * g⁻¹)) (n : ℤ) : P (g ^ n)
Full source 
/-- To show a property of all powers of `g` it suffices to show it is closed under multiplication
by `g` and `g⁻¹` on the right. For subgroups generated by more than one element, see
`Subgroup.closure_induction_right`. -/
@[to_additive "To show a property of all multiples of `g` it suffices to show it is closed under
addition by `g` and `-g` on the right. For additive subgroups generated by more than one element,
see `AddSubgroup.closure_induction_right`."]
lemma zpow_induction_right {g : G} {P : G → Prop} (h_one : P (1 : G))
    (h_mul : ∀ a, P a → P (a * g)) (h_inv : ∀ a, P a → P (a * g⁻¹)) (n : ℤ) : P (g ^ n) := by
  induction n with
  | hz => rwa [zpow_zero]
  | hp n ih =>
    rw [zpow_add_one]
    exact h_mul _ ih
  | hn n ih =>
    rw [zpow_sub_one]
    exact h_inv _ ih
Right Induction Principle for Integer Powers in Groups
Informal description
Let $G$ be a group and $g \in G$. To prove that a property $P$ holds for all integer powers $g^n$ (for $n \in \mathbb{Z}$), it suffices to show: 1. $P$ holds for the identity element ($P(1)$), 2. For any $a \in G$, if $P(a)$ holds then $P(a \cdot g)$ holds, and 3. For any $a \in G$, if $P(a)$ holds then $P(a \cdot g^{-1})$ holds.
div_eq_of_eq_mul' theorem
{a b c : G} (h : a = b * c) : a / b = c
Full source 
@[to_additive]
theorem div_eq_of_eq_mul' {a b c : G} (h : a = b * c) : a / b = c := by
  rw [h, div_eq_mul_inv, mul_comm, inv_mul_cancel_left]
Division by $b$ of $a = b \cdot c$ equals $c$
Informal description
Let $G$ be a group, and let $a, b, c \in G$ such that $a = b \cdot c$. Then $a / b = c$.
mul_div_mul_left_eq_div theorem
(a b c : G) : c * a / (c * b) = a / b
Full source 
@[to_additive (attr := simp)]
theorem mul_div_mul_left_eq_div (a b c : G) : c * a / (c * b) = a / b := by
  rw [div_eq_mul_inv, mul_inv_rev, mul_comm b⁻¹ c⁻¹, mul_comm c a, mul_assoc, ← mul_assoc c,
    mul_inv_cancel, one_mul, div_eq_mul_inv]
Simplification of $(c \cdot a) / (c \cdot b)$ to $a / b$ in a group
Informal description
For any elements $a, b, c$ in a group $G$, the expression $(c \cdot a) / (c \cdot b)$ simplifies to $a / b$.
mul_eq_of_eq_div' theorem
(h : b = c / a) : a * b = c
Full source 
@[to_additive]
theorem mul_eq_of_eq_div' (h : b = c / a) : a * b = c := by
  rw [h, div_eq_mul_inv, mul_comm c, mul_inv_cancel_left]
Multiplication from Division Equality: $a \cdot b = c$ given $b = c / a$
Informal description
For elements $a, b, c$ in a group $G$, if $b = c / a$, then $a \cdot b = c$.
div_div_self' theorem
(a b : G) : a / (a / b) = b
Full source 
@[to_additive sub_sub_self]
theorem div_div_self' (a b : G) : a / (a / b) = b := by simp
Double Division Identity: $a / (a / b) = b$
Informal description
For any elements $a$ and $b$ in a group $G$, the operation $a / (a / b)$ simplifies to $b$.
div_eq_div_mul_div theorem
(a b c : G) : a / b = c / b * (a / c)
Full source 
@[to_additive]
theorem div_eq_div_mul_div (a b c : G) : a / b = c / b * (a / c) := by simp [mul_left_comm c]
Quotient Decomposition: $a / b = (c / b) \cdot (a / c)$
Informal description
For any elements $a, b, c$ in a group $G$, the quotient $a / b$ can be expressed as $(c / b) \cdot (a / c)$.
div_div_cancel theorem
(a b : G) : a / (a / b) = b
Full source 
@[to_additive (attr := simp)]
theorem div_div_cancel (a b : G) : a / (a / b) = b :=
  div_div_self' a b
Double Division Identity: $a / (a / b) = b$
Informal description
For any elements $a$ and $b$ in a group $G$, the operation $a / (a / b)$ simplifies to $b$.
div_div_cancel_left theorem
(a b : G) : a / b / a = b⁻¹
Full source 
@[to_additive (attr := simp)]
theorem div_div_cancel_left (a b : G) : a / b / a = b⁻¹ := by simp
Double Division Equals Inverse: $(a / b) / a = b^{-1}$
Informal description
For any elements $a, b$ in a group $G$, the following equality holds: $(a / b) / a = b^{-1}$.
mul_div_cancel_left theorem
(a b : G) : a * b / a = b
Full source 
@[to_additive (attr := simp)]
theorem mul_div_cancel_left (a b : G) : a * b / a = b := by rw [div_eq_inv_mul, inv_mul_cancel_left]
Left Cancellation in Group Division: $(a * b) / a = b$
Informal description
For any elements $a$ and $b$ in a group $G$, the expression $(a * b) / a$ simplifies to $b$.
mul_div_cancel theorem
(a b : G) : a * (b / a) = b
Full source 
@[to_additive (attr := simp)]
theorem mul_div_cancel (a b : G) : a * (b / a) = b := by
  rw [← mul_div_assoc, mul_div_cancel_left]
Right Cancellation in Group Division: $a * (b / a) = b$
Informal description
For any elements $a$ and $b$ in a group $G$, the expression $a * (b / a)$ simplifies to $b$.
div_mul_cancel_left theorem
(a b : G) : a / (a * b) = b⁻¹
Full source 
@[to_additive (attr := simp)]
theorem div_mul_cancel_left (a b : G) : a / (a * b) = b⁻¹ := by rw [← inv_div, mul_div_cancel_left]
Quotient of Product Equals Inverse: $a / (a * b) = b^{-1}$
Informal description
For any elements $a$ and $b$ in a group $G$, the quotient $a / (a * b)$ equals the inverse of $b$, i.e., $a / (a * b) = b^{-1}$.
mul_mul_inv_cancel'_right theorem
(a b : G) : a * (b * a⁻¹) = b
Full source 
@[to_additive]
theorem mul_mul_inv_cancel'_right (a b : G) : a * (b * a⁻¹) = b := by
  rw [← div_eq_mul_inv, mul_div_cancel a b]
Right Conjugation Cancellation: $a * (b * a^{-1}) = b$
Informal description
For any elements $a$ and $b$ in a group $G$, the expression $a * (b * a^{-1})$ simplifies to $b$.
mul_mul_div_cancel theorem
(a b c : G) : a * c * (b / c) = a * b
Full source 
@[to_additive (attr := simp)]
theorem mul_mul_div_cancel (a b c : G) : a * c * (b / c) = a * b := by
  rw [mul_assoc, mul_div_cancel]
Group Multiplication-Division Cancellation: $a \cdot c \cdot (b / c) = a \cdot b$
Informal description
For any elements $a, b, c$ in a group $G$, the expression $a \cdot c \cdot (b / c)$ simplifies to $a \cdot b$.
div_mul_mul_cancel theorem
(a b c : G) : a / c * (b * c) = a * b
Full source 
@[to_additive (attr := simp)]
theorem div_mul_mul_cancel (a b c : G) : a / c * (b * c) = a * b := by
  rw [mul_left_comm, div_mul_cancel, mul_comm]
Division and Multiplication Cancellation in Groups: $(a / c) \cdot (b \cdot c) = a \cdot b$
Informal description
For any elements $a, b, c$ in a group $G$, the following equality holds: $(a / c) \cdot (b \cdot c) = a \cdot b$.
div_mul_div_cancel' theorem
(a b c : G) : a / b * (c / a) = c / b
Full source 
@[to_additive (attr := simp)]
theorem div_mul_div_cancel' (a b c : G) : a / b * (c / a) = c / b := by
  rw [mul_comm]; apply div_mul_div_cancel
Group Division-Multiplication Identity: $(a / b) \cdot (c / a) = c / b$
Informal description
For any elements $a, b, c$ in a group $G$, the following identity holds: $(a / b) \cdot (c / a) = c / b$.
mul_div_div_cancel theorem
(a b c : G) : a * b / (a / c) = b * c
Full source 
@[to_additive (attr := simp)]
theorem mul_div_div_cancel (a b c : G) : a * b / (a / c) = b * c := by
  rw [← div_mul, mul_div_cancel_left]
Group Division-Multiplication Cancellation: $(a \cdot b) / (a / c) = b \cdot c$
Informal description
For any elements $a$, $b$, and $c$ in a group $G$, the following equality holds: $(a \cdot b) / (a / c) = b \cdot c$.
div_div_div_cancel_left theorem
(a b c : G) : c / a / (c / b) = b / a
Full source 
@[to_additive (attr := simp)]
theorem div_div_div_cancel_left (a b c : G) : c / a / (c / b) = b / a := by
  rw [← inv_div b c, div_inv_eq_mul, mul_comm, div_mul_div_cancel]
Triple Division Cancellation Identity: $(c / a) / (c / b) = b / a$
Informal description
For any elements $a, b, c$ in a group $G$, the following identity holds: $(c / a) / (c / b) = b / a$.
div_eq_div_iff_mul_eq_mul theorem
: a / b = c / d ↔ a * d = c * b
Full source 
@[to_additive]
theorem div_eq_div_iff_mul_eq_mul : a / b = c / d ↔ a * d = c * b := by
  rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, eq_comm, div_eq_iff_eq_mul']
  simp only [mul_comm, eq_comm]
Division Equality via Cross-Multiplication: $a / b = c / d \leftrightarrow a \cdot d = c \cdot b$
Informal description
For any elements $a, b, c, d$ in a group, the equality $a / b = c / d$ holds if and only if $a \cdot d = c \cdot b$.
multiplicative_of_symmetric_of_isTotal theorem
(hsymm : Symmetric p) (hf_swap : ∀ {a b}, p a b → f a b * f b a = 1) (hmul : ∀ {a b c}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c) {a b c : α} (pab : p a b) (pbc : p b c) (pac : p a c) : f a c = f a b * f b c
Full source 
@[to_additive additive_of_symmetric_of_isTotal]
lemma multiplicative_of_symmetric_of_isTotal
    (hsymm : Symmetric p) (hf_swap : ∀ {a b}, p a b → f a b * f b a = 1)
    (hmul : ∀ {a b c}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c)
    {a b c : α} (pab : p a b) (pbc : p b c) (pac : p a c) : f a c = f a b * f b c := by
  have hmul' : ∀ {b c}, r b c → p a b → p b c → p a c → f a c = f a b * f b c := by
    intros b c rbc pab pbc pac
    obtain rab | rba := total_of r a b
    · exact hmul rab rbc pab pbc pac
    rw [← one_mul (f a c), ← hf_swap pab, mul_assoc]
    obtain rac | rca := total_of r a c
    · rw [hmul rba rac (hsymm pab) pac pbc]
    · rw [hmul rbc rca pbc (hsymm pac) (hsymm pab), mul_assoc, hf_swap (hsymm pac), mul_one]
  obtain rbc | rcb := total_of r b c
  · exact hmul' rbc pab pbc pac
  · rw [hmul' rcb pac (hsymm pbc) pab, mul_assoc, hf_swap (hsymm pbc), mul_one]
Multiplicativity under Symmetric Relation and Total Order Conditions
Informal description
Let $p$ be a symmetric relation on a type $\alpha$, and let $f : \alpha \times \alpha \to M$ be a function to a monoid $M$. Suppose that: 1. For any $a, b \in \alpha$, if $p(a, b)$ holds, then $f(a, b) \cdot f(b, a) = 1$. 2. For any $a, b, c \in \alpha$, if $r(a, b)$ and $r(b, c)$ hold, and $p(a, b)$, $p(b, c)$, and $p(a, c)$ all hold, then $f(a, c) = f(a, b) \cdot f(b, c)$. Then for any $a, b, c \in \alpha$ such that $p(a, b)$, $p(b, c)$, and $p(a, c)$ all hold, we have $f(a, c) = f(a, b) \cdot f(b, c)$.
multiplicative_of_isTotal theorem
(p : α → Prop) (hswap : ∀ {a b}, p a → p b → f a b * f b a = 1) (hmul : ∀ {a b c}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c) {a b c : α} (pa : p a) (pb : p b) (pc : p c) : f a c = f a b * f b c
Full source 
/-- If a binary function from a type equipped with a total relation `r` to a monoid is
  anti-symmetric (i.e. satisfies `f a b * f b a = 1`), in order to show it is multiplicative
  (i.e. satisfies `f a c = f a b * f b c`), we may assume `r a b` and `r b c` are satisfied.
  We allow restricting to a subset specified by a predicate `p`. -/
@[to_additive additive_of_isTotal "If a binary function from a type equipped with a total relation
`r` to an additive monoid is anti-symmetric (i.e. satisfies `f a b + f b a = 0`), in order to show
it is additive (i.e. satisfies `f a c = f a b + f b c`), we may assume `r a b` and `r b c` are
satisfied. We allow restricting to a subset specified by a predicate `p`."]
theorem multiplicative_of_isTotal (p : α → Prop) (hswap : ∀ {a b}, p a → p b → f a b * f b a = 1)
    (hmul : ∀ {a b c}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c) {a b c : α}
    (pa : p a) (pb : p b) (pc : p c) : f a c = f a b * f b c := by
  apply multiplicative_of_symmetric_of_isTotal (fun a b => p a ∧ p b) r f fun _ _ => And.symm
  · simp_rw [and_imp]; exact @hswap
  · exact fun rab rbc pab _pbc pac => hmul rab rbc pab.1 pab.2 pac.2
  exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]
Multiplicativity of Anti-Symmetric Function under Total Relation
Informal description
Let $\alpha$ be a type equipped with a total relation $r$, $M$ a monoid, and $f \colon \alpha \times \alpha \to M$ a binary function. Suppose: 1. For any $a, b \in \alpha$ satisfying a predicate $p$, $f(a, b) \cdot f(b, a) = 1$. 2. For any $a, b, c \in \alpha$ with $r(a, b)$, $r(b, c)$, and $p(a)$, $p(b)$, $p(c)$ all holding, $f(a, c) = f(a, b) \cdot f(b, c)$. Then for any $a, b, c \in \alpha$ with $p(a)$, $p(b)$, $p(c)$ all holding, we have $f(a, c) = f(a, b) \cdot f(b, c)$.
hom_coe_pow theorem
{F : Type*} [Monoid F] (c : F → M → M) (h1 : c 1 = id) (hmul : ∀ f g, c (f * g) = c f ∘ c g) (f : F) : ∀ n, c (f ^ n) = (c f)^[n]
Full source 
/-- An auxiliary lemma that can be used to prove `⇑(f ^ n) = ⇑f^[n]`. -/
@[to_additive]
lemma hom_coe_pow {F : Type*} [Monoid F] (c : F → M → M) (h1 : c 1 = id)
    (hmul : ∀ f g, c (f * g) = c f ∘ c g) (f : F) : ∀ n, c (f ^ n) = (c f)^[n]
  | 0 => by
    rw [pow_zero, h1]
    rfl
  | n + 1 => by rw [pow_succ, iterate_succ, hmul, hom_coe_pow c h1 hmul f n]
Iteration of Monoid Homomorphism on Powers: $c(f^n) = c(f)^{[n]}$
Informal description
Let $F$ be a monoid and $c \colon F \to (M \to M)$ be a function such that: 1. $c(1)$ is the identity function on $M$, 2. For any $f, g \in F$, $c(f \cdot g) = c(f) \circ c(g)$. Then for any $f \in F$ and natural number $n$, the function $c(f^n)$ equals the $n$-th iterate of $c(f)$, i.e., $c(f^n) = c(f)^{[n]}$.