# 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 `Mathlib/Algebra/Group/Defs.lean`.

source
@[simp]
theorem pow_dite {α : Type u_1} {β : Type u_2} [Pow α β] (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
source
@[simp]
theorem dite_smul {α : Type u_1} {β : Type u_2} [SMul β α] (p : Prop) [Decidable p] (a : α) (b : p → β) (c : ¬p → β) :
(if h : p then b h else c h) • a = if h : p then b h • a else c h • a
source
@[simp]
theorem dite_pow {α : Type u_1} {β : Type u_2} [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
source
@[simp]
theorem smul_dite {α : Type u_1} {β : Type u_2} [SMul β α] (p : Prop) [Decidable p] (a : p → α) (b : ¬p → α) (c : β) :
(c • if h : p then a h else b h) = if h : p then c • a h else c • b h
source
@[simp]
theorem pow_ite {α : Type u_1} {β : Type u_2} [Pow α β] (p : Prop) [Decidable p] (a : α) (b c : β) :
(a ^ if p then b else c) = if p then a ^ b else a ^ c
source
@[simp]
theorem ite_smul {α : Type u_1} {β : Type u_2} [SMul β α] (p : Prop) [Decidable p] (a : α) (b c : β) :
(if p then b else c) • a = if p then b • a else c • a
source
@[simp]
theorem ite_pow {α : Type u_1} {β : Type u_2} [Pow α β] (p : Prop) [Decidable p] (a b : α) (c : β) :
(if p then a else b) ^ c = if p then a ^ c else b ^ c
source
@[simp]
theorem smul_ite {α : Type u_1} {β : Type u_2} [SMul β α] (p : Prop) [Decidable p] (a b : α) (c : β) :
(c • if p then a else b) = if p then c • a else c • b
source
@[simp]
theorem vadd_ite {α : Type u_1} {β : Type u_2} [VAdd β α] (p : Prop) [Decidable p] (a b : α) (c : β) :
(c +ᵥ if p then a else b) = if p then c +ᵥ a else c +ᵥ b
source
@[simp]
theorem dite_vadd {α : Type u_1} {β : Type u_2} [VAdd β α] (p : Prop) [Decidable p] (a : α) (b : p → β) (c : ¬p → β) :
(if h : p then b h else c h) +ᵥ a = if h : p then b h +ᵥ a else c h +ᵥ a
source
@[simp]
theorem vadd_dite {α : Type u_1} {β : Type u_2} [VAdd β α] (p : Prop) [Decidable p] (a : p → α) (b : ¬p → α) (c : β) :
(c +ᵥ if h : p then a h else b h) = if h : p then c +ᵥ a h else c +ᵥ b h
source
@[simp]
theorem ite_vadd {α : Type u_1} {β : Type u_2} [VAdd β α] (p : Prop) [Decidable p] (a : α) (b c : β) :
(if p then b else c) +ᵥ a = if p then b +ᵥ a else c +ᵥ a
source
instance Semigroup.to_isAssociative {α : Type u_1} [Semigroup α] :
Std.Associative fun (x1 x2 : α) => x1 * x2
source
instance AddSemigroup.to_isAssociative {α : Type u_1} [AddSemigroup α] :
Std.Associative fun (x1 x2 : α) => x1 + x2
source
@[simp]
theorem comp_mul_left {α : Type u_1} [Semigroup α] (x y : α) :
((fun (x_1 : α) => x * x_1) ∘ fun (x : α) => y * x) = fun (x_1 : α) => x * y * x_1

Composing two multiplications on the left by `y` then `x` is equal to a multiplication on the left by `x * y`.

source
@[simp]
theorem comp_add_left {α : Type u_1} [AddSemigroup α] (x y : α) :
((fun (x_1 : α) => x + x_1) ∘ fun (x : α) => y + x) = fun (x_1 : α) => x + y + x_1

Composing two additions on the left by `y` then `x` is equal to an addition on the left by `x + y`.

source
@[simp]
theorem comp_mul_right {α : Type u_1} [Semigroup α] (x y : α) :
((fun (x_1 : α) => x_1 * x) ∘ fun (x : α) => x * y) = fun (x_1 : α) => x_1 * (y * x)

Composing two multiplications on the right by `y` and `x` is equal to a multiplication on the right by `y * x`.

source
@[simp]
theorem comp_add_right {α : Type u_1} [AddSemigroup α] (x y : α) :
((fun (x_1 : α) => x_1 + x) ∘ fun (x : α) => x + y) = fun (x_1 : α) => x_1 + (y + x)

Composing two additions on the right by `y` and `x` is equal to an addition on the right by `y + x`.

source
instance CommMagma.to_isCommutative {G : Type u_3} [CommMagma G] :
Std.Commutative fun (x1 x2 : G) => x1 * x2
source
instance AddCommMagma.to_isCommutative {G : Type u_3} [AddCommMagma G] :
Std.Commutative fun (x1 x2 : G) => x1 + x2
source
instance Semigroup.to_isLawfulIdentity {M : Type u_4} [MulOneClass M] :
Std.LawfulIdentity (fun (x1 x2 : M) => x1 * x2) 1
source
instance AddSemigroup.to_isLawfulIdentity {M : Type u_4} [AddZeroClass M] :
Std.LawfulIdentity (fun (x1 x2 : M) => x1 + x2) 0
source
theorem ite_mul_one {M : Type u_4} [MulOneClass M] {P : Prop} [Decidable P] {a b : M} :
(if P then a * b else 1) = (if P then a else 1) * if P then b else 1
source
theorem ite_add_zero {M : Type u_4} [AddZeroClass M] {P : Prop} [Decidable P] {a b : M} :
(if P then a + b else 0) = (if P then a else 0) + if P then b else 0
source
theorem ite_one_mul {M : Type u_4} [MulOneClass M] {P : Prop} [Decidable P] {a b : M} :
(if P then 1 else a * b) = (if P then 1 else a) * if P then 1 else b
source
theorem ite_zero_add {M : Type u_4} [AddZeroClass M] {P : Prop} [Decidable P] {a b : M} :
(if P then 0 else a + b) = (if P then 0 else a) + if P then 0 else b
source
theorem eq_one_iff_eq_one_of_mul_eq_one {M : Type u_4} [MulOneClass M] {a b : M} (h : a * b = 1) :
a = 1 ↔ b = 1
source
theorem eq_zero_iff_eq_zero_of_add_eq_zero {M : Type u_4} [AddZeroClass M] {a b : M} (h : a + b = 0) :
a = 0 ↔ b = 0
source
theorem one_mul_eq_id {M : Type u_4} [MulOneClass M] :
(fun (x : M) => 1 * x) = id
source
theorem zero_add_eq_id {M : Type u_4} [AddZeroClass M] :
(fun (x : M) => 0 + x) = id
source
theorem mul_one_eq_id {M : Type u_4} [MulOneClass M] :
(fun (x : M) => x * 1) = id
source
theorem add_zero_eq_id {M : Type u_4} [AddZeroClass M] :
(fun (x : M) => x + 0) = id
source
theorem mul_left_comm {G : Type u_3} [CommSemigroup G] (a b c : G) :
a * (b * c) = b * (a * c)
source
theorem add_left_comm {G : Type u_3} [AddCommSemigroup G] (a b c : G) :
a + (b + c) = b + (a + c)
source
theorem mul_right_comm {G : Type u_3} [CommSemigroup G] (a b c : G) :
a * b * c = a * c * b
source
theorem add_right_comm {G : Type u_3} [AddCommSemigroup G] (a b c : G) :
a + b + c = a + c + b
source
theorem mul_mul_mul_comm {G : Type u_3} [CommSemigroup G] (a b c d : G) :
a * b * (c * d) = a * c * (b * d)
source
theorem add_add_add_comm {G : Type u_3} [AddCommSemigroup G] (a b c d : G) :
a + b + (c + d) = a + c + (b + d)
source
theorem mul_mul_mul_comm' {G : Type u_3} [CommSemigroup G] (a b c d : G) :
a * b * c * d = a * c * b * d
source
theorem add_add_add_comm' {G : Type u_3} [AddCommSemigroup G] (a b c d : G) :
a + b + c + d = a + c + b + d
source
theorem mul_rotate {G : Type u_3} [CommSemigroup G] (a b c : G) :
a * b * c = b * c * a
source
theorem add_rotate {G : Type u_3} [AddCommSemigroup G] (a b c : G) :
a + b + c = b + c + a
source
theorem mul_rotate' {G : Type u_3} [CommSemigroup G] (a b c : G) :
a * (b * c) = b * (c * a)
source
theorem add_rotate' {G : Type u_3} [AddCommSemigroup G] (a b c : G) :
a + (b + c) = b + (c + a)
source
theorem pow_boole {M : Type u_4} [Monoid M] (P : Prop) [Decidable P] (a : M) :
(a ^ if P then 1 else 0) = if P then a else 1
source
theorem boole_nsmul {M : Type u_4} [AddMonoid M] (P : Prop) [Decidable P] (a : M) :
(if P then 1 else 0) • a = if P then a else 0
source
theorem pow_mul_pow_sub {M : Type u_4} [Monoid M] {m n : ℕ} (a : M) (h : m ≤ n) :
a ^ m * a ^ (n - m) = a ^ n
source
theorem nsmul_add_sub_nsmul {M : Type u_4} [AddMonoid M] {m n : ℕ} (a : M) (h : m ≤ n) :
m • a + (n - m) • a = n • a
source
theorem pow_sub_mul_pow {M : Type u_4} [Monoid M] {m n : ℕ} (a : M) (h : m ≤ n) :
a ^ (n - m) * a ^ m = a ^ n
source
theorem sub_nsmul_nsmul_add {M : Type u_4} [AddMonoid M] {m n : ℕ} (a : M) (h : m ≤ n) :
(n - m) • a + m • a = n • a
source
theorem mul_pow_sub_one {M : Type u_4} [Monoid M] {n : ℕ} (hn : n ≠ 0) (a : M) :
a * a ^ (n - 1) = a ^ n
source
theorem sub_one_nsmul_add {M : Type u_4} [AddMonoid M] {n : ℕ} (hn : n ≠ 0) (a : M) :
a + (n - 1) • a = n • a
source
theorem pow_sub_one_mul {M : Type u_4} [Monoid M] {n : ℕ} (hn : n ≠ 0) (a : M) :
a ^ (n - 1) * a = a ^ n
source
theorem add_sub_one_nsmul {M : Type u_4} [AddMonoid M] {n : ℕ} (hn : n ≠ 0) (a : M) :
(n - 1) • a + a = n • a
source
theorem pow_eq_pow_mod {M : Type u_4} [Monoid M] {a : M} {n : ℕ} (m : ℕ) (ha : a ^ n = 1) :
a ^ m = a ^ (m % n)

If `x ^ n = 1`, then `x ^ m` is the same as `x ^ (m % n)`

source
theorem nsmul_eq_mod_nsmul {M : Type u_4} [AddMonoid M] {a : M} {n : ℕ} (m : ℕ) (ha : n • a = 0) :
m • a = (m % n) • a

If `n • x = 0`, then `m • x` is the same as `(m % n) • x`

source
theorem pow_mul_pow_eq_one {M : Type u_4} [Monoid M] {a b : M} (n : ℕ) :
a * b = 1 → a ^ n * b ^ n = 1
source
theorem nsmul_add_nsmul_eq_zero {M : Type u_4} [AddMonoid M] {a b : M} (n : ℕ) :
a + b = 0 → n • a + n • b = 0
source
@[simp]
theorem mul_left_iterate {M : Type u_4} [Monoid M] (a : M) (n : ℕ) :
(fun (x : M) => a * x)^[n] = fun (x : M) => a ^ n * x
source
@[simp]
theorem add_left_iterate {M : Type u_4} [AddMonoid M] (a : M) (n : ℕ) :
(fun (x : M) => a + x)^[n] = fun (x : M) => n • a + x
source
@[simp]
theorem mul_right_iterate {M : Type u_4} [Monoid M] (a : M) (n : ℕ) :
(fun (x : M) => x * a)^[n] = fun (x : M) => x * a ^ n
source
@[simp]
theorem add_right_iterate {M : Type u_4} [AddMonoid M] (a : M) (n : ℕ) :
(fun (x : M) => x + a)^[n] = fun (x : M) => x + n • a
source
theorem mul_left_iterate_apply {M : Type u_4} [Monoid M] {n : ℕ} (a b : M) :
(fun (x : M) => a * x)^[n] b = a ^ n * b

Version of `mul_left_iterate` that is fully applied, for `rw`.

source
theorem add_left_iterate_apply {M : Type u_4} [AddMonoid M] {n : ℕ} (a b : M) :
(fun (x : M) => a + x)^[n] b = n • a + b

Version of `add_left_iterate` that is fully applied, for `rw`.

source
theorem mul_right_iterate_apply {M : Type u_4} [Monoid M] {n : ℕ} (a b : M) :
(fun (x : M) => x * a)^[n] b = b * a ^ n

Version of `mul_right_iterate` that is fully applied, for `rw`.

source
theorem add_right_iterate_apply {M : Type u_4} [AddMonoid M] {n : ℕ} (a b : M) :
(fun (x : M) => x + a)^[n] b = b + n • a

Version of `add_right_iterate` that is fully applied, for `rw`.

source
theorem mul_left_iterate_apply_one {M : Type u_4} [Monoid M] {n : ℕ} (a : M) :
(fun (x : M) => a * x)^[n] 1 = a ^ n
source
theorem add_left_iterate_apply_zero {M : Type u_4} [AddMonoid M] {n : ℕ} (a : M) :
(fun (x : M) => a + x)^[n] 0 = n • a
source
theorem mul_right_iterate_apply_one {M : Type u_4} [Monoid M] {n : ℕ} (a : M) :
(fun (x : M) => x * a)^[n] 1 = a ^ n
source
theorem add_right_iterate_apply_zero {M : Type u_4} [AddMonoid M] {n : ℕ} (a : M) :
(fun (x : M) => x + a)^[n] 0 = n • a
source
@[simp]
theorem pow_iterate {M : Type u_4} [Monoid M] (k n : ℕ) :
(fun (x : M) => x ^ k)^[n] = fun (x : M) => x ^ k ^ n
source
@[simp]
theorem nsmul_iterate {M : Type u_4} [AddMonoid M] (k n : ℕ) :
(fun (x : M) => k • x)^[n] = fun (x : M) => k ^ n • x
source
theorem inv_unique {M : Type u_4} [CommMonoid M] {x y z : M} (hy : x * y = 1) (hz : x * z = 1) :
y = z
source
theorem neg_unique {M : Type u_4} [AddCommMonoid M] {x y z : M} (hy : x + y = 0) (hz : x + z = 0) :
y = z
source
theorem mul_pow {M : Type u_4} [CommMonoid M] (a b : M) (n : ℕ) :
(a * b) ^ n = a ^ n * b ^ n
source
theorem nsmul_add {M : Type u_4} [AddCommMonoid M] (a b : M) (n : ℕ) :
n • (a + b) = n • a + n • b
source
@[simp]
theorem mul_eq_left {M : Type u_4} [Monoid M] [IsLeftCancelMul M] {a b : M} :
a * b = a ↔ b = 1
source
@[simp]
theorem add_eq_left {M : Type u_4} [AddMonoid M] [IsLeftCancelAdd M] {a b : M} :
a + b = a ↔ b = 0
source
@[simp]
theorem left_eq_mul {M : Type u_4} [Monoid M] [IsLeftCancelMul M] {a b : M} :
a = a * b ↔ b = 1
source
@[simp]
theorem left_eq_add {M : Type u_4} [AddMonoid M] [IsLeftCancelAdd M] {a b : M} :
a = a + b ↔ b = 0
source
theorem mul_ne_left {M : Type u_4} [Monoid M] [IsLeftCancelMul M] {a b : M} :
a * b ≠ a ↔ b ≠ 1
source
theorem add_ne_left {M : Type u_4} [AddMonoid M] [IsLeftCancelAdd M] {a b : M} :
a + b ≠ a ↔ b ≠ 0
source
theorem left_ne_mul {M : Type u_4} [Monoid M] [IsLeftCancelMul M] {a b : M} :
a ≠ a * b ↔ b ≠ 1
source
theorem left_ne_add {M : Type u_4} [AddMonoid M] [IsLeftCancelAdd M] {a b : M} :
a ≠ a + b ↔ b ≠ 0
source
@[simp]
theorem mul_eq_right {M : Type u_4} [Monoid M] [IsRightCancelMul M] {a b : M} :
a * b = b ↔ a = 1
source
@[simp]
theorem add_eq_right {M : Type u_4} [AddMonoid M] [IsRightCancelAdd M] {a b : M} :
a + b = b ↔ a = 0
source
@[simp]
theorem right_eq_mul {M : Type u_4} [Monoid M] [IsRightCancelMul M] {a b : M} :
b = a * b ↔ a = 1
source
@[simp]
theorem right_eq_add {M : Type u_4} [AddMonoid M] [IsRightCancelAdd M] {a b : M} :
b = a + b ↔ a = 0
source
theorem mul_ne_right {M : Type u_4} [Monoid M] [IsRightCancelMul M] {a b : M} :
a * b ≠ b ↔ a ≠ 1
source
theorem add_ne_right {M : Type u_4} [AddMonoid M] [IsRightCancelAdd M] {a b : M} :
a + b ≠ b ↔ a ≠ 0
source
theorem right_ne_mul {M : Type u_4} [Monoid M] [IsRightCancelMul M] {a b : M} :
b ≠ a * b ↔ a ≠ 1
source
theorem right_ne_add {M : Type u_4} [AddMonoid M] [IsRightCancelAdd M] {a b : M} :
b ≠ a + b ↔ a ≠ 0
source
theorem eq_iff_eq_of_mul_eq_mul {α : Type u_1} [CancelCommMonoid α] {a b c d : α} (h : a * b = c * d) :
a = c ↔ b = d
source
theorem eq_iff_eq_of_add_eq_add {α : Type u_1} [AddCancelCommMonoid α] {a b c d : α} (h : a + b = c + d) :
a = c ↔ b = d
source
theorem ne_iff_ne_of_mul_eq_mul {α : Type u_1} [CancelCommMonoid α] {a b c d : α} (h : a * b = c * d) :
a ≠ c ↔ b ≠ d
source
theorem ne_iff_ne_of_add_eq_add {α : Type u_1} [AddCancelCommMonoid α] {a b c d : α} (h : a + b = c + d) :
a ≠ c ↔ b ≠ d
source
@[simp]
theorem inv_involutive {G : Type u_3} [InvolutiveInv G] :
Function.Involutive Inv.inv
source
@[simp]
theorem neg_involutive {G : Type u_3} [InvolutiveNeg G] :
Function.Involutive Neg.neg
source
@[simp]
theorem inv_surjective {G : Type u_3} [InvolutiveInv G] :
Function.Surjective Inv.inv
source
@[simp]
theorem neg_surjective {G : Type u_3} [InvolutiveNeg G] :
Function.Surjective Neg.neg
source
theorem inv_injective {G : Type u_3} [InvolutiveInv G] :
Function.Injective Inv.inv
source
theorem neg_injective {G : Type u_3} [InvolutiveNeg G] :
Function.Injective Neg.neg
source
@[simp]
theorem inv_inj {G : Type u_3} [InvolutiveInv G] {a b : G} :
a⁻¹ = b⁻¹ ↔ a = b
source
@[simp]
theorem neg_inj {G : Type u_3} [InvolutiveNeg G] {a b : G} :
-a = -b ↔ a = b
source
theorem inv_eq_iff_eq_inv {G : Type u_3} [InvolutiveInv G] {a b : G} :
a⁻¹ = b ↔ a = b⁻¹
source
theorem neg_eq_iff_eq_neg {G : Type u_3} [InvolutiveNeg G] {a b : G} :
-a = b ↔ a = -b
source
theorem inv_comp_inv (G : Type u_3) [InvolutiveInv G] :
Inv.inv ∘ Inv.inv = id
source
theorem neg_comp_neg (G : Type u_3) [InvolutiveNeg G] :
Neg.neg ∘ Neg.neg = id
source
theorem leftInverse_inv (G : Type u_3) [InvolutiveInv G] :
Function.LeftInverse (fun (a : G) => a⁻¹) fun (a : G) => a⁻¹
source
theorem leftInverse_neg (G : Type u_3) [InvolutiveNeg G] :
Function.LeftInverse (fun (a : G) => -a) fun (a : G) => -a
source
theorem rightInverse_inv (G : Type u_3) [InvolutiveInv G] :
Function.RightInverse (fun (a : G) => a⁻¹) fun (a : G) => a⁻¹
source
theorem rightInverse_neg (G : Type u_3) [InvolutiveNeg G] :
Function.RightInverse (fun (a : G) => -a) fun (a : G) => -a
source
theorem mul_one_div {G : Type u_3} [DivInvMonoid G] (x y : G) :
x * (1 / y) = x / y
source
theorem add_zero_sub {G : Type u_3} [SubNegMonoid G] (x y : G) :
x + (0 - y) = x - y
source
theorem mul_div_assoc' {G : Type u_3} [DivInvMonoid G] (a b c : G) :
a * (b / c) = a * b / c
source
theorem add_sub_assoc' {G : Type u_3} [SubNegMonoid G] (a b c : G) :
a + (b - c) = a + b - c
source
theorem mul_div {G : Type u_3} [DivInvMonoid G] (a b c : G) :
a * (b / c) = a * b / c
source
theorem add_sub {G : Type u_3} [SubNegMonoid G] (a b c : G) :
a + (b - c) = a + b - c
source
theorem div_eq_mul_one_div {G : Type u_3} [DivInvMonoid G] (a b : G) :
a / b = a * (1 / b)
source
theorem sub_eq_add_zero_sub {G : Type u_3} [SubNegMonoid G] (a b : G) :
a - b = a + (0 - b)
source
@[simp]
theorem div_one {G : Type u_3} [DivInvOneMonoid G] (a : G) :
a / 1 = a
source
@[simp]
theorem sub_zero {G : Type u_3} [SubNegZeroMonoid G] (a : G) :
a - 0 = a
source
theorem one_div_one {G : Type u_3} [DivInvOneMonoid G] :
1 / 1 = 1
source
theorem zero_sub_zero {G : Type u_3} [SubNegZeroMonoid G] :
0 - 0 = 0
source
theorem eq_inv_of_mul_eq_one_right {α : Type u_1} [DivisionMonoid α] {a b : α} (h : a * b = 1) :
b = a⁻¹
source
theorem eq_neg_of_add_eq_zero_right {α : Type u_1} [SubtractionMonoid α] {a b : α} (h : a + b = 0) :
b = -a
source
theorem eq_one_div_of_mul_eq_one_left {α : Type u_1} [DivisionMonoid α] {a b : α} (h : b * a = 1) :
b = 1 / a
source
theorem eq_zero_sub_of_add_eq_zero_left {α : Type u_1} [SubtractionMonoid α] {a b : α} (h : b + a = 0) :
b = 0 - a
source
theorem eq_one_div_of_mul_eq_one_right {α : Type u_1} [DivisionMonoid α] {a b : α} (h : a * b = 1) :
b = 1 / a
source
theorem eq_zero_sub_of_add_eq_zero_right {α : Type u_1} [SubtractionMonoid α] {a b : α} (h : a + b = 0) :
b = 0 - a
source
theorem eq_of_div_eq_one {α : Type u_1} [DivisionMonoid α] {a b : α} (h : a / b = 1) :
a = b
source
theorem eq_of_sub_eq_zero {α : Type u_1} [SubtractionMonoid α] {a b : α} (h : a - b = 0) :
a = b
source
theorem eq_of_inv_mul_eq_one {α : Type u_1} [DivisionMonoid α] {a b : α} (h : a⁻¹ * b = 1) :
a = b
source
theorem eq_of_neg_add_eq_zero {α : Type u_1} [SubtractionMonoid α] {a b : α} (h : -a + b = 0) :
a = b
source
theorem eq_of_mul_inv_eq_one {α : Type u_1} [DivisionMonoid α] {a b : α} (h : a * b⁻¹ = 1) :
a = b
source
theorem eq_of_add_neg_eq_zero {α : Type u_1} [SubtractionMonoid α] {a b : α} (h : a + -b = 0) :
a = b
source
theorem div_ne_one_of_ne {α : Type u_1} [DivisionMonoid α] {a b : α} :
a ≠ b → a / b ≠ 1
source
theorem sub_ne_zero_of_ne {α : Type u_1} [SubtractionMonoid α] {a b : α} :
a ≠ b → a - b ≠ 0
source
theorem one_div_mul_one_div_rev {α : Type u_1} [DivisionMonoid α] (a b : α) :
1 / a * (1 / b) = 1 / (b * a)
source
theorem zero_sub_add_zero_sub_rev {α : Type u_1} [SubtractionMonoid α] (a b : α) :
0 - a + (0 - b) = 0 - (b + a)
source
theorem inv_div_left {α : Type u_1} [DivisionMonoid α] (a b : α) :
a⁻¹ / b = (b * a)⁻¹
source
theorem neg_sub_left {α : Type u_1} [SubtractionMonoid α] (a b : α) :
-a - b = -(b + a)
source
@[simp]
theorem inv_div {α : Type u_1} [DivisionMonoid α] (a b : α) :
(a / b)⁻¹ = b / a
source
@[simp]
theorem neg_sub {α : Type u_1} [SubtractionMonoid α] (a b : α) :
-(a - b) = b - a
source
theorem one_div_div {α : Type u_1} [DivisionMonoid α] (a b : α) :
1 / (a / b) = b / a
source
theorem zero_sub_sub {α : Type u_1} [SubtractionMonoid α] (a b : α) :
0 - (a - b) = b - a
source
theorem one_div_one_div {α : Type u_1} [DivisionMonoid α] (a : α) :
1 / (1 / a) = a
source
theorem zero_sub_zero_sub {α : Type u_1} [SubtractionMonoid α] (a : α) :
0 - (0 - a) = a
source
theorem div_eq_div_iff_comm {α : Type u_1} [DivisionMonoid α] (a b c : α) {d : α} :
a / b = c / d ↔ b / a = d / c
source
theorem sub_eq_sub_iff_comm {α : Type u_1} [SubtractionMonoid α] (a b c : α) {d : α} :
a - b = c - d ↔ b - a = d - c
source
@[instance 100]
instance DivisionMonoid.toDivInvOneMonoid {α : Type u_1} [DivisionMonoid α] :
DivInvOneMonoid α
Equations

- DivisionMonoid.toDivInvOneMonoid = { toDivInvMonoid := inst✝.toDivInvMonoid, inv_one := ⋯ }

source
@[instance 100]
instance SubtractionMonoid.toSubNegZeroMonoid {α : Type u_1} [SubtractionMonoid α] :
SubNegZeroMonoid α
Equations

- SubtractionMonoid.toSubNegZeroMonoid = { toSubNegMonoid := inst✝.toSubNegMonoid, neg_zero := ⋯ }

source
@[simp]
theorem inv_pow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℕ) :
a⁻¹ ^ n = (a ^ n)⁻¹
source
@[simp]
theorem neg_nsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℕ) :
n • -a = -(n • a)
source
@[simp]
theorem one_zpow {α : Type u_1} [DivisionMonoid α] (n : ℤ) :
1 ^ n = 1
source
theorem zsmul_zero {α : Type u_1} [SubtractionMonoid α] (n : ℤ) :
n • 0 = 0
source
@[simp]
theorem zpow_neg {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) :
a ^ (-n) = (a ^ n)⁻¹
source
@[simp]
theorem neg_zsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) :
-n • a = -(n • a)
source
theorem mul_zpow_neg_one {α : Type u_1} [DivisionMonoid α] (a b : α) :
(a * b) ^ (-1) = b ^ (-1) * a ^ (-1)
source
theorem neg_one_zsmul_add {α : Type u_1} [SubtractionMonoid α] (a b : α) :
-1 • (a + b) = -1 • b + -1 • a
source
theorem inv_zpow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) :
a⁻¹ ^ n = (a ^ n)⁻¹
source
theorem zsmul_neg {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) :
n • -a = -(n • a)
source
@[simp]
theorem inv_zpow' {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) :
a⁻¹ ^ n = a ^ (-n)
source
@[simp]
theorem zsmul_neg' {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) :
n • -a = -n • a
source
theorem one_div_pow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℕ) :
(1 / a) ^ n = 1 / a ^ n
source
theorem nsmul_zero_sub {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℕ) :
n • (0 - a) = 0 - n • a
source
theorem one_div_zpow {α : Type u_1} [DivisionMonoid α] (a : α) (n : ℤ) :
(1 / a) ^ n = 1 / a ^ n
source
theorem zsmul_zero_sub {α : Type u_1} [SubtractionMonoid α] (a : α) (n : ℤ) :
n • (0 - a) = 0 - n • a
source
@[simp]
theorem inv_eq_one {α : Type u_1} [DivisionMonoid α] {a : α} :
a⁻¹ = 1 ↔ a = 1
source
@[simp]
theorem neg_eq_zero {α : Type u_1} [SubtractionMonoid α] {a : α} :
-a = 0 ↔ a = 0
source
@[simp]
theorem one_eq_inv {α : Type u_1} [DivisionMonoid α] {a : α} :
1 = a⁻¹ ↔ a = 1
source
@[simp]
theorem zero_eq_neg {α : Type u_1} [SubtractionMonoid α] {a : α} :
0 = -a ↔ a = 0
source
theorem inv_ne_one {α : Type u_1} [DivisionMonoid α] {a : α} :
a⁻¹ ≠ 1 ↔ a ≠ 1
source
theorem neg_ne_zero {α : Type u_1} [SubtractionMonoid α] {a : α} :
-a ≠ 0 ↔ a ≠ 0
source
theorem eq_of_one_div_eq_one_div {α : Type u_1} [DivisionMonoid α] {a b : α} (h : 1 / a = 1 / b) :
a = b
source
theorem eq_of_zero_sub_eq_zero_sub {α : Type u_1} [SubtractionMonoid α] {a b : α} (h : 0 - a = 0 - b) :
a = b
source
theorem zpow_mul {α : Type u_1} [DivisionMonoid α] (a : α) (m n : ℤ) :
a ^ (m * n) = (a ^ m) ^ n
source
theorem mul_zsmul' {α : Type u_1} [SubtractionMonoid α] (a : α) (m n : ℤ) :
(m * n) • a = n • m • a
source
theorem zpow_mul' {α : Type u_1} [DivisionMonoid α] (a : α) (m n : ℤ) :
a ^ (m * n) = (a ^ n) ^ m
source
theorem mul_zsmul {α : Type u_1} [SubtractionMonoid α] (a : α) (m n : ℤ) :
(m * n) • a = m • n • a
source
theorem zpow_comm {α : Type u_1} [DivisionMonoid α] (a : α) (m n : ℤ) :
(a ^ m) ^ n = (a ^ n) ^ m
source
theorem zsmul_comm {α : Type u_1} [SubtractionMonoid α] (a : α) (m n : ℤ) :
n • m • a = m • n • a
source
theorem div_div_eq_mul_div {α : Type u_1} [DivisionMonoid α] (a b c : α) :
a / (b / c) = a * c / b
source
theorem sub_sub_eq_add_sub {α : Type u_1} [SubtractionMonoid α] (a b c : α) :
a - (b - c) = a + c - b
source
@[simp]
theorem div_inv_eq_mul {α : Type u_1} [DivisionMonoid α] (a b : α) :
a / b⁻¹ = a * b
source
@[simp]
theorem sub_neg_eq_add {α : Type u_1} [SubtractionMonoid α] (a b : α) :
a - -b = a + b
source
theorem div_mul_eq_div_div_swap {α : Type u_1} [DivisionMonoid α] (a b c : α) :
a / (b * c) = a / c / b
source
theorem sub_add_eq_sub_sub_swap {α : Type u_1} [SubtractionMonoid α] (a b c : α) :
a - (b + c) = a - c - b
source
theorem mul_inv {α : Type u_1} [DivisionCommMonoid α] (a b : α) :
(a * b)⁻¹ = a⁻¹ * b⁻¹
source
theorem neg_add {α : Type u_1} [SubtractionCommMonoid α] (a b : α) :
-(a + b) = -a + -b
source
theorem inv_div' {α : Type u_1} [DivisionCommMonoid α] (a b : α) :
(a / b)⁻¹ = a⁻¹ / b⁻¹
source
theorem neg_sub' {α : Type u_1} [SubtractionCommMonoid α] (a b : α) :
-(a - b) = -a - -b
source
theorem div_eq_inv_mul {α : Type u_1} [DivisionCommMonoid α] (a b : α) :
a / b = b⁻¹ * a
source
theorem sub_eq_neg_add {α : Type u_1} [SubtractionCommMonoid α] (a b : α) :
a - b = -b + a
source
theorem inv_mul_eq_div {α : Type u_1} [DivisionCommMonoid α] (a b : α) :
a⁻¹ * b = b / a
source
theorem neg_add_eq_sub {α : Type u_1} [SubtractionCommMonoid α] (a b : α) :
-a + b = b - a
source
theorem inv_div_comm {α : Type u_1} [DivisionCommMonoid α] (a b : α) :
a⁻¹ / b = b⁻¹ / a
source
theorem neg_sub_comm {α : Type u_1} [SubtractionCommMonoid α] (a b : α) :
-a - b = -b - a
source
theorem inv_mul' {α : Type u_1} [DivisionCommMonoid α] (a b : α) :
(a * b)⁻¹ = a⁻¹ / b
source
theorem neg_add' {α : Type u_1} [SubtractionCommMonoid α] (a b : α) :
-(a + b) = -a - b
source
theorem inv_div_inv {α : Type u_1} [DivisionCommMonoid α] (a b : α) :
a⁻¹ / b⁻¹ = b / a
source
theorem neg_sub_neg {α : Type u_1} [SubtractionCommMonoid α] (a b : α) :
-a - -b = b - a
source
theorem inv_inv_div_inv {α : Type u_1} [DivisionCommMonoid α] (a b : α) :
(a⁻¹ / b⁻¹)⁻¹ = a / b
source
theorem neg_neg_sub_neg {α : Type u_1} [SubtractionCommMonoid α] (a b : α) :
-(-a - -b) = a - b
source
theorem one_div_mul_one_div {α : Type u_1} [DivisionCommMonoid α] (a b : α) :
1 / a * (1 / b) = 1 / (a * b)
source
theorem zero_sub_add_zero_sub {α : Type u_1} [SubtractionCommMonoid α] (a b : α) :
0 - a + (0 - b) = 0 - (a + b)
source
theorem div_right_comm {α : Type u_1} [DivisionCommMonoid α] (a b c : α) :
a / b / c = a / c / b
source
theorem sub_right_comm {α : Type u_1} [SubtractionCommMonoid α] (a b c : α) :
a - b - c = a - c - b
source
theorem div_div {α : Type u_1} [DivisionCommMonoid α] (a b c : α) :
a / b / c = a / (b * c)
source
theorem sub_sub {α : Type u_1} [SubtractionCommMonoid α] (a b c : α) :
a - b - c = a - (b + c)
source
theorem div_mul {α : Type u_1} [DivisionCommMonoid α] (a b c : α) :
a / b * c = a / (b / c)
source
theorem sub_add {α : Type u_1} [SubtractionCommMonoid α] (a b c : α) :
a - b + c = a - (b - c)
source
theorem mul_div_left_comm {α : Type u_1} [DivisionCommMonoid α] (a b c : α) :
a * (b / c) = b * (a / c)
source
theorem add_sub_left_comm {α : Type u_1} [SubtractionCommMonoid α] (a b c : α) :
a + (b - c) = b + (a - c)
source
theorem mul_div_right_comm {α : Type u_1} [DivisionCommMonoid α] (a b c : α) :
a * b / c = a / c * b
source
theorem add_sub_right_comm {α : Type u_1} [SubtractionCommMonoid α] (a b c : α) :
a + b - c = a - c + b
source
theorem div_mul_eq_div_div {α : Type u_1} [DivisionCommMonoid α] (a b c : α) :
a / (b * c) = a / b / c
source
theorem sub_add_eq_sub_sub {α : Type u_1} [SubtractionCommMonoid α] (a b c : α) :
a - (b + c) = a - b - c
source
theorem div_mul_eq_mul_div {α : Type u_1} [DivisionCommMonoid α] (a b c : α) :
a / b * c = a * c / b
source
theorem sub_add_eq_add_sub {α : Type u_1} [SubtractionCommMonoid α] (a b c : α) :
a - b + c = a + c - b
source
theorem one_div_mul_eq_div {α : Type u_1} [DivisionCommMonoid α] (a b : α) :
1 / a * b = b / a
source
theorem zero_sub_add_eq_sub {α : Type u_1} [SubtractionCommMonoid α] (a b : α) :
0 - a + b = b - a
source
theorem mul_comm_div {α : Type u_1} [DivisionCommMonoid α] (a b c : α) :
a / b * c = a * (c / b)
source
theorem add_comm_sub {α : Type u_1} [SubtractionCommMonoid α] (a b c : α) :
a - b + c = a + (c - b)
source
theorem div_mul_comm {α : Type u_1} [DivisionCommMonoid α] (a b c : α) :
a / b * c = c / b * a
source
theorem sub_add_comm {α : Type u_1} [SubtractionCommMonoid α] (a b c : α) :
a - b + c = c - b + a
source
theorem div_mul_eq_div_mul_one_div {α : Type u_1} [DivisionCommMonoid α] (a b c : α) :
a / (b * c) = a / b * (1 / c)
source
theorem sub_add_eq_sub_add_zero_sub {α : Type u_1} [SubtractionCommMonoid α] (a b c : α) :
a - (b + c) = a - b + (0 - c)
source
theorem div_div_div_eq {α : Type u_1} [DivisionCommMonoid α] (a b c d : α) :
a / b / (c / d) = a * d / (b * c)
source
theorem sub_sub_sub_eq {α : Type u_1} [SubtractionCommMonoid α] (a b c d : α) :
a - b - (c - d) = a + d - (b + c)
source
theorem div_div_div_comm {α : Type u_1} [DivisionCommMonoid α] (a b c d : α) :
a / b / (c / d) = a / c / (b / d)
source
theorem sub_sub_sub_comm {α : Type u_1} [SubtractionCommMonoid α] (a b c d : α) :
a - b - (c - d) = a - c - (b - d)
source
theorem div_mul_div_comm {α : Type u_1} [DivisionCommMonoid α] (a b c d : α) :
a / b * (c / d) = a * c / (b * d)
source
theorem sub_add_sub_comm {α : Type u_1} [SubtractionCommMonoid α] (a b c d : α) :
a - b + (c - d) = a + c - (b + d)
source
theorem mul_div_mul_comm {α : Type u_1} [DivisionCommMonoid α] (a b c d : α) :
a * b / (c * d) = a / c * (b / d)
source
theorem add_sub_add_comm {α : Type u_1} [SubtractionCommMonoid α] (a b c d : α) :
a + b - (c + d) = a - c + (b - d)
source
theorem mul_zpow {α : Type u_1} [DivisionCommMonoid α] (a b : α) (n : ℤ) :
(a * b) ^ n = a ^ n * b ^ n
source
theorem zsmul_add {α : Type u_1} [SubtractionCommMonoid α] (a b : α) (n : ℤ) :
n • (a + b) = n • a + n • b
source
theorem div_pow {α : Type u_1} [DivisionCommMonoid α] (a b : α) (n : ℕ) :
(a / b) ^ n = a ^ n / b ^ n
source
theorem nsmul_sub {α : Type u_1} [SubtractionCommMonoid α] (a b : α) (n : ℕ) :
n • (a - b) = n • a - n • b
source
theorem div_zpow {α : Type u_1} [DivisionCommMonoid α] (a b : α) (n : ℤ) :
(a / b) ^ n = a ^ n / b ^ n
source
theorem zsmul_sub {α : Type u_1} [SubtractionCommMonoid α] (a b : α) (n : ℤ) :
n • (a - b) = n • a - n • b
source
@[simp]
theorem div_eq_inv_self {G : Type u_3} [Group G] {a b : G} :
a / b = b⁻¹ ↔ a = 1
source
@[simp]
theorem sub_eq_neg_self {G : Type u_3} [AddGroup G] {a b : G} :
a - b = -b ↔ a = 0
source
theorem mul_left_surjective {G : Type u_3} [Group G] (a : G) :
Function.Surjective fun (x : G) => a * x
source
theorem add_left_surjective {G : Type u_3} [AddGroup G] (a : G) :
Function.Surjective fun (x : G) => a + x
source
theorem mul_right_surjective {G : Type u_3} [Group G] (a : G) :
Function.Surjective fun (x : G) => x * a
source
theorem add_right_surjective {G : Type u_3} [AddGroup G] (a : G) :
Function.Surjective fun (x : G) => x + a
source
theorem eq_mul_inv_of_mul_eq {G : Type u_3} [Group G] {a b c : G} (h : a * c = b) :
a = b * c⁻¹
source
theorem eq_add_neg_of_add_eq {G : Type u_3} [AddGroup G] {a b c : G} (h : a + c = b) :
a = b + -c
source
theorem eq_inv_mul_of_mul_eq {G : Type u_3} [Group G] {a b c : G} (h : b * a = c) :
a = b⁻¹ * c
source
theorem eq_neg_add_of_add_eq {G : Type u_3} [AddGroup G] {a b c : G} (h : b + a = c) :
a = -b + c
source
theorem inv_mul_eq_of_eq_mul {G : Type u_3} [Group G] {a b c : G} (h : b = a * c) :
a⁻¹ * b = c
source
theorem neg_add_eq_of_eq_add {G : Type u_3} [AddGroup G] {a b c : G} (h : b = a + c) :
-a + b = c
source
theorem mul_inv_eq_of_eq_mul {G : Type u_3} [Group G] {a b c : G} (h : a = c * b) :
a * b⁻¹ = c
source
theorem add_neg_eq_of_eq_add {G : Type u_3} [AddGroup G] {a b c : G} (h : a = c + b) :
a + -b = c
source
theorem eq_mul_of_mul_inv_eq {G : Type u_3} [Group G] {a b c : G} (h : a * c⁻¹ = b) :
a = b * c
source
theorem eq_add_of_add_neg_eq {G : Type u_3} [AddGroup G] {a b c : G} (h : a + -c = b) :
a = b + c
source
theorem eq_mul_of_inv_mul_eq {G : Type u_3} [Group G] {a b c : G} (h : b⁻¹ * a = c) :
a = b * c
source
theorem eq_add_of_neg_add_eq {G : Type u_3} [AddGroup G] {a b c : G} (h : -b + a = c) :
a = b + c
source
theorem mul_eq_of_eq_inv_mul {G : Type u_3} [Group G] {a b c : G} (h : b = a⁻¹ * c) :
a * b = c
source
theorem add_eq_of_eq_neg_add {G : Type u_3} [AddGroup G] {a b c : G} (h : b = -a + c) :
a + b = c
source
theorem mul_eq_of_eq_mul_inv {G : Type u_3} [Group G] {a b c : G} (h : a = c * b⁻¹) :
a * b = c
source
theorem add_eq_of_eq_add_neg {G : Type u_3} [AddGroup G] {a b c : G} (h : a = c + -b) :
a + b = c
source
theorem mul_eq_one_iff_eq_inv {G : Type u_3} [Group G] {a b : G} :
a * b = 1 ↔ a = b⁻¹
source
theorem add_eq_zero_iff_eq_neg {G : Type u_3} [AddGroup G] {a b : G} :
a + b = 0 ↔ a = -b
source
theorem mul_eq_one_iff_inv_eq {G : Type u_3} [Group G] {a b : G} :
a * b = 1 ↔ a⁻¹ = b
source
theorem add_eq_zero_iff_neg_eq {G : Type u_3} [AddGroup G] {a b : G} :
a + b = 0 ↔ -a = b
source
theorem mul_eq_one_iff_eq_inv' {G : Type u_3} [Group G] {a b : G} :
a * b = 1 ↔ b = a⁻¹

Variant of `mul_eq_one_iff_eq_inv` with swapped equality.

source
theorem add_eq_zero_iff_eq_neg' {G : Type u_3} [AddGroup G] {a b : G} :
a + b = 0 ↔ b = -a
source
theorem mul_eq_one_iff_inv_eq' {G : Type u_3} [Group G] {a b : G} :
a * b = 1 ↔ b⁻¹ = a

Variant of `mul_eq_one_iff_inv_eq` with swapped equality.

source
theorem add_eq_zero_iff_neg_eq' {G : Type u_3} [AddGroup G] {a b : G} :
a + b = 0 ↔ -b = a
source
theorem eq_inv_iff_mul_eq_one {G : Type u_3} [Group G] {a b : G} :
a = b⁻¹ ↔ a * b = 1
source
theorem eq_neg_iff_add_eq_zero {G : Type u_3} [AddGroup G] {a b : G} :
a = -b ↔ a + b = 0
source
theorem inv_eq_iff_mul_eq_one {G : Type u_3} [Group G] {a b : G} :
a⁻¹ = b ↔ a * b = 1
source
theorem neg_eq_iff_add_eq_zero {G : Type u_3} [AddGroup G] {a b : G} :
-a = b ↔ a + b = 0
source
theorem eq_mul_inv_iff_mul_eq {G : Type u_3} [Group G] {a b c : G} :
a = b * c⁻¹ ↔ a * c = b
source
theorem eq_add_neg_iff_add_eq {G : Type u_3} [AddGroup G] {a b c : G} :
a = b + -c ↔ a + c = b
source
theorem eq_inv_mul_iff_mul_eq {G : Type u_3} [Group G] {a b c : G} :
a = b⁻¹ * c ↔ b * a = c
source
theorem eq_neg_add_iff_add_eq {G : Type u_3} [AddGroup G] {a b c : G} :
a = -b + c ↔ b + a = c
source
theorem inv_mul_eq_iff_eq_mul {G : Type u_3} [Group G] {a b c : G} :
a⁻¹ * b = c ↔ b = a * c
source
theorem neg_add_eq_iff_eq_add {G : Type u_3} [AddGroup G] {a b c : G} :
-a + b = c ↔ b = a + c
source
theorem mul_inv_eq_iff_eq_mul {G : Type u_3} [Group G] {a b c : G} :
a * b⁻¹ = c ↔ a = c * b
source
theorem add_neg_eq_iff_eq_add {G : Type u_3} [AddGroup G] {a b c : G} :
a + -b = c ↔ a = c + b
source
theorem mul_inv_eq_one {G : Type u_3} [Group G] {a b : G} :
a * b⁻¹ = 1 ↔ a = b
source
theorem add_neg_eq_zero {G : Type u_3} [AddGroup G] {a b : G} :
a + -b = 0 ↔ a = b
source
theorem inv_mul_eq_one {G : Type u_3} [Group G] {a b : G} :
a⁻¹ * b = 1 ↔ a = b
source
theorem neg_add_eq_zero {G : Type u_3} [AddGroup G] {a b : G} :
-a + b = 0 ↔ a = b
source
@[simp]
theorem conj_eq_one_iff {G : Type u_3} [Group G] {a b : G} :
a * b * a⁻¹ = 1 ↔ b = 1
source
@[simp]
theorem conj_eq_zero_iff {G : Type u_3} [AddGroup G] {a b : G} :
a + b + -a = 0 ↔ b = 0
source
theorem div_left_injective {G : Type u_3} [Group G] {b : G} :
Function.Injective fun (a : G) => a / b
source
theorem sub_left_injective {G : Type u_3} [AddGroup G] {b : G} :
Function.Injective fun (a : G) => a - b
source
theorem div_right_injective {G : Type u_3} [Group G] {b : G} :
Function.Injective fun (a : G) => b / a
source
theorem sub_right_injective {G : Type u_3} [AddGroup G] {b : G} :
Function.Injective fun (a : G) => b - a
source
@[simp]
theorem div_mul_cancel_right {G : Type u_3} [Group G] (a b : G) :
a / (b * a) = b⁻¹
source
@[simp]
theorem sub_add_cancel_right {G : Type u_3} [AddGroup G] (a b : G) :
a - (b + a) = -b
source
@[simp]
theorem mul_div_mul_right_eq_div {G : Type u_3} [Group G] (a b c : G) :
a * c / (b * c) = a / b
source
@[simp]
theorem add_sub_add_right_eq_sub {G : Type u_3} [AddGroup G] (a b c : G) :
a + c - (b + c) = a - b
source
theorem eq_div_of_mul_eq' {G : Type u_3} [Group G] {a b c : G} (h : a * c = b) :
a = b / c
source
theorem eq_sub_of_add_eq {G : Type u_3} [AddGroup G] {a b c : G} (h : a + c = b) :
a = b - c
source
theorem div_eq_of_eq_mul'' {G : Type u_3} [Group G] {a b c : G} (h : a = c * b) :
a / b = c
source
theorem sub_eq_of_eq_add {G : Type u_3} [AddGroup G] {a b c : G} (h : a = c + b) :
a - b = c
source
theorem eq_mul_of_div_eq {G : Type u_3} [Group G] {a b c : G} (h : a / c = b) :
a = b * c
source
theorem eq_add_of_sub_eq {G : Type u_3} [AddGroup G] {a b c : G} (h : a - c = b) :
a = b + c
source
theorem mul_eq_of_eq_div {G : Type u_3} [Group G] {a b c : G} (h : a = c / b) :
a * b = c
source
theorem add_eq_of_eq_sub {G : Type u_3} [AddGroup G] {a b c : G} (h : a = c - b) :
a + b = c
source
@[simp]
theorem div_right_inj {G : Type u_3} [Group G] {a b c : G} :
a / b = a / c ↔ b = c
source
@[simp]
theorem sub_right_inj {G : Type u_3} [AddGroup G] {a b c : G} :
a - b = a - c ↔ b = c
source
@[simp]
theorem div_left_inj {G : Type u_3} [Group G] {a b c : G} :
b / a = c / a ↔ b = c
source
@[simp]
theorem sub_left_inj {G : Type u_3} [AddGroup G] {a b c : G} :
b - a = c - a ↔ b = c
source
@[simp]
theorem div_mul_div_cancel {G : Type u_3} [Group G] (a b c : G) :
a / b * (b / c) = a / c
source
@[simp]
theorem sub_add_sub_cancel {G : Type u_3} [AddGroup G] (a b c : G) :
a - b + (b - c) = a - c
source
@[simp]
theorem div_div_div_cancel_right {G : Type u_3} [Group G] (a b c : G) :
a / c / (b / c) = a / b
source
@[simp]
theorem sub_sub_sub_cancel_right {G : Type u_3} [AddGroup G] (a b c : G) :
a - c - (b - c) = a - b
source
theorem div_eq_one {G : Type u_3} [Group G] {a b : G} :
a / b = 1 ↔ a = b
source
theorem sub_eq_zero {G : Type u_3} [AddGroup G] {a b : G} :
a - b = 0 ↔ a = b
source
theorem div_eq_one_of_eq {G : Type u_3} [Group G] {a b : G} :
a = b → a / b = 1

Alias of the reverse direction of `div_eq_one`.

source
theorem sub_eq_zero_of_eq {G : Type u_3} [AddGroup G] {a b : G} :
a = b → a - b = 0

Alias of the reverse direction of `sub_eq_zero`.

source
theorem div_ne_one {G : Type u_3} [Group G] {a b : G} :
a / b ≠ 1 ↔ a ≠ b
source
theorem sub_ne_zero {G : Type u_3} [AddGroup G] {a b : G} :
a - b ≠ 0 ↔ a ≠ b
source
@[simp]
theorem div_eq_self {G : Type u_3} [Group G] {a b : G} :
a / b = a ↔ b = 1
source
@[simp]
theorem sub_eq_self {G : Type u_3} [AddGroup G] {a b : G} :
a - b = a ↔ b = 0
source
theorem eq_div_iff_mul_eq' {G : Type u_3} [Group G] {a b c : G} :
a = b / c ↔ a * c = b
source
theorem eq_sub_iff_add_eq {G : Type u_3} [AddGroup G] {a b c : G} :
a = b - c ↔ a + c = b
source
theorem div_eq_iff_eq_mul {G : Type u_3} [Group G] {a b c : G} :
a / b = c ↔ a = c * b
source
theorem sub_eq_iff_eq_add {G : Type u_3} [AddGroup G] {a b c : G} :
a - b = c ↔ a = c + b
source
theorem eq_iff_eq_of_div_eq_div {G : Type u_3} [Group G] {a b c d : G} (H : a / b = c / d) :
a = b ↔ c = d
source
theorem eq_iff_eq_of_sub_eq_sub {G : Type u_3} [AddGroup G] {a b c d : G} (H : a - b = c - d) :
a = b ↔ c = d
source
theorem leftInverse_div_mul_left {G : Type u_3} [Group G] (c : G) :
Function.LeftInverse (fun (x : G) => x / c) fun (x : G) => x * c
source
theorem leftInverse_sub_add_left {G : Type u_3} [AddGroup G] (c : G) :
Function.LeftInverse (fun (x : G) => x - c) fun (x : G) => x + c
source
theorem leftInverse_mul_left_div {G : Type u_3} [Group G] (c : G) :
Function.LeftInverse (fun (x : G) => x * c) fun (x : G) => x / c
source
theorem leftInverse_add_left_sub {G : Type u_3} [AddGroup G] (c : G) :
Function.LeftInverse (fun (x : G) => x + c) fun (x : G) => x - c
source
theorem leftInverse_mul_right_inv_mul {G : Type u_3} [Group G] (c : G) :
Function.LeftInverse (fun (x : G) => c * x) fun (x : G) => c⁻¹ * x
source
theorem leftInverse_add_right_neg_add {G : Type u_3} [AddGroup G] (c : G) :
Function.LeftInverse (fun (x : G) => c + x) fun (x : G) => -c + x
source
theorem leftInverse_inv_mul_mul_right {G : Type u_3} [Group G] (c : G) :
Function.LeftInverse (fun (x : G) => c⁻¹ * x) fun (x : G) => c * x
source
theorem leftInverse_neg_add_add_right {G : Type u_3} [AddGroup G] (c : G) :
Function.LeftInverse (fun (x : G) => -c + x) fun (x : G) => c + x
source
@[simp]
theorem pow_natAbs_eq_one {G : Type u_3} [Group G] {a : G} {n : ℤ} :
a ^ n.natAbs = 1 ↔ a ^ n = 1
source
@[simp]
theorem natAbs_nsmul_eq_zero {G : Type u_3} [AddGroup G] {a : G} {n : ℤ} :
n.natAbs • a = 0 ↔ n • a = 0
source
theorem pow_sub {G : Type u_3} [Group G] (a : G) {m n : ℕ} (h : n ≤ m) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
source
theorem sub_nsmul {G : Type u_3} [AddGroup G] (a : G) {m n : ℕ} (h : n ≤ m) :
(m - n) • a = m • a + -(n • a)
source
theorem inv_pow_sub {G : Type u_3} [Group G] (a : G) {m n : ℕ} (h : n ≤ m) :
a⁻¹ ^ (m - n) = (a ^ m)⁻¹ * a ^ n
source
theorem sub_nsmul_neg {G : Type u_3} [AddGroup G] (a : G) {m n : ℕ} (h : n ≤ m) :
(m - n) • -a = -(m • a) + n • a
source
theorem zpow_add_one {G : Type u_3} [Group G] (a : G) (n : ℤ) :
a ^ (n + 1) = a ^ n * a
source
theorem add_one_zsmul {G : Type u_3} [AddGroup G] (a : G) (n : ℤ) :
(n + 1) • a = n • a + a
source
theorem zpow_sub_one {G : Type u_3} [Group G] (a : G) (n : ℤ) :
a ^ (n - 1) = a ^ n * a⁻¹
source
theorem sub_one_zsmul {G : Type u_3} [AddGroup G] (a : G) (n : ℤ) :
(n - 1) • a = n • a + -a
source
theorem zpow_add {G : Type u_3} [Group G] (a : G) (m n : ℤ) :
a ^ (m + n) = a ^ m * a ^ n
source
theorem add_zsmul {G : Type u_3} [AddGroup G] (a : G) (m n : ℤ) :
(m + n) • a = m • a + n • a
source
theorem zpow_one_add {G : Type u_3} [Group G] (a : G) (n : ℤ) :
a ^ (1 + n) = a * a ^ n
source
theorem one_add_zsmul {G : Type u_3} [AddGroup G] (a : G) (n : ℤ) :
(1 + n) • a = a + n • a
source
theorem mul_self_zpow {G : Type u_3} [Group G] (a : G) (n : ℤ) :
a * a ^ n = a ^ (n + 1)
source
theorem add_zsmul_self {G : Type u_3} [AddGroup G] (a : G) (n : ℤ) :
a + n • a = (n + 1) • a
source
theorem mul_zpow_self {G : Type u_3} [Group G] (a : G) (n : ℤ) :
a ^ n * a = a ^ (n + 1)
source
theorem add_self_zsmul {G : Type u_3} [AddGroup G] (a : G) (n : ℤ) :
n • a + a = (n + 1) • a
source
theorem zpow_sub {G : Type u_3} [Group G] (a : G) (m n : ℤ) :
a ^ (m - n) = a ^ m * (a ^ n)⁻¹
source
theorem sub_zsmul {G : Type u_3} [AddGroup G] (a : G) (m n : ℤ) :
(m - n) • a = m • a + -(n • a)
source
theorem zpow_natCast_sub_natCast {G : Type u_3} [Group G] (a : G) (m n : ℕ) :
a ^ (↑m - ↑n) = a ^ m / a ^ n
source
theorem natCast_sub_natCast_zsmul {G : Type u_3} [AddGroup G] (a : G) (m n : ℕ) :
(↑m - ↑n) • a = m • a - n • a
source
theorem zpow_natCast_sub_one {G : Type u_3} [Group G] (a : G) (n : ℕ) :
a ^ (↑n - 1) = a ^ n / a
source
theorem natCast_sub_one_zsmul {G : Type u_3} [AddGroup G] (a : G) (n : ℕ) :
(↑n - 1) • a = n • a - a
source
theorem zpow_one_sub_natCast {G : Type u_3} [Group G] (a : G) (n : ℕ) :
a ^ (1 - ↑n) = a / a ^ n
source
theorem one_sub_natCast_zsmul {G : Type u_3} [AddGroup G] (a : G) (n : ℕ) :
(1 - ↑n) • a = a - n • a
source
theorem zpow_mul_comm {G : Type u_3} [Group G] (a : G) (m n : ℤ) :
a ^ m * a ^ n = a ^ n * a ^ m
source
theorem zsmul_add_comm {G : Type u_3} [AddGroup G] (a : G) (m n : ℤ) :
m • a + n • a = n • a + m • a
source
theorem mul_zpow_mul {G : Type u_3} [Group G] (a b : G) (n : ℤ) :
(a * b) ^ n * a = a * (b * a) ^ n
source
theorem add_zsmul_add {G : Type u_3} [AddGroup G] (a b : G) (n : ℤ) :
n • (a + b) + a = a + n • (b + a)
source
theorem zpow_eq_zpow_emod {G : Type u_3} [Group G] {x : G} (m : ℤ) {n : ℤ} (h : x ^ n = 1) :
x ^ m = x ^ (m % n)
source
theorem zpow_eq_zpow_emod' {G : Type u_3} [Group G] {x : G} (m : ℤ) {n : ℕ} (h : x ^ n = 1) :
x ^ m = x ^ (m % ↑n)
source
@[simp]
theorem zpow_iterate {G : Type u_3} [Group G] (k : ℤ) (n : ℕ) :
(fun (x : G) => x ^ k)^[n] = fun (x : G) => x ^ k ^ n
source
@[simp]
theorem zsmul_iterate {G : Type u_3} [AddGroup G] (k : ℤ) (n : ℕ) :
(fun (x : G) => k • x)^[n] = fun (x : G) => k ^ n • x
source
theorem zpow_induction_left {G : Type u_3} [Group G] {g : G} {P : G → Prop} (h_one : P 1) (h_mul : ∀ (a : G), P a → P (g * a)) (h_inv : ∀ (a : G), P a → P (g⁻¹ * a)) (n : ℤ) :
P (g ^ n)

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`.

source
theorem zsmul_induction_left {G : Type u_3} [AddGroup G] {g : G} {P : G → Prop} (h_zero : P 0) (h_add : ∀ (a : G), P a → P (g + a)) (h_neg : ∀ (a : G), P a → P (-g + a)) (n : ℤ) :
P (n • g)

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`.

source
theorem zpow_induction_right {G : Type u_3} [Group G] {g : G} {P : G → Prop} (h_one : P 1) (h_mul : ∀ (a : G), P a → P (a * g)) (h_inv : ∀ (a : G), P a → P (a * g⁻¹)) (n : ℤ) :
P (g ^ n)

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`.

source
theorem zsmul_induction_right {G : Type u_3} [AddGroup G] {g : G} {P : G → Prop} (h_zero : P 0) (h_add : ∀ (a : G), P a → P (a + g)) (h_neg : ∀ (a : G), P a → P (a + -g)) (n : ℤ) :
P (n • g)

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`.

source
theorem div_eq_of_eq_mul' {G : Type u_3} [CommGroup G] {a b c : G} (h : a = b * c) :
a / b = c
source
theorem sub_eq_of_eq_add' {G : Type u_3} [AddCommGroup G] {a b c : G} (h : a = b + c) :
a - b = c
source
@[simp]
theorem mul_div_mul_left_eq_div {G : Type u_3} [CommGroup G] (a b c : G) :
c * a / (c * b) = a / b
source
@[simp]
theorem add_sub_add_left_eq_sub {G : Type u_3} [AddCommGroup G] (a b c : G) :
c + a - (c + b) = a - b
source
theorem eq_div_of_mul_eq'' {G : Type u_3} [CommGroup G] {a b c : G} (h : c * a = b) :
a = b / c
source
theorem eq_sub_of_add_eq' {G : Type u_3} [AddCommGroup G] {a b c : G} (h : c + a = b) :
a = b - c
source
theorem eq_mul_of_div_eq' {G : Type u_3} [CommGroup G] {a b c : G} (h : a / b = c) :
a = b * c
source
theorem eq_add_of_sub_eq' {G : Type u_3} [AddCommGroup G] {a b c : G} (h : a - b = c) :
a = b + c
source
theorem mul_eq_of_eq_div' {G : Type u_3} [CommGroup G] {a b c : G} (h : b = c / a) :
a * b = c
source
theorem add_eq_of_eq_sub' {G : Type u_3} [AddCommGroup G] {a b c : G} (h : b = c - a) :
a + b = c
source
theorem div_div_self' {G : Type u_3} [CommGroup G] (a b : G) :
a / (a / b) = b
source
theorem sub_sub_self {G : Type u_3} [AddCommGroup G] (a b : G) :
a - (a - b) = b
source
theorem div_eq_div_mul_div {G : Type u_3} [CommGroup G] (a b c : G) :
a / b = c / b * (a / c)
source
theorem sub_eq_sub_add_sub {G : Type u_3} [AddCommGroup G] (a b c : G) :
a - b = c - b + (a - c)
source
@[simp]
theorem div_div_cancel {G : Type u_3} [CommGroup G] (a b : G) :
a / (a / b) = b
source
@[simp]
theorem sub_sub_cancel {G : Type u_3} [AddCommGroup G] (a b : G) :
a - (a - b) = b
source
@[simp]
theorem div_div_cancel_left {G : Type u_3} [CommGroup G] (a b : G) :
a / b / a = b⁻¹
source
@[simp]
theorem sub_sub_cancel_left {G : Type u_3} [AddCommGroup G] (a b : G) :
a - b - a = -b
source
theorem eq_div_iff_mul_eq'' {G : Type u_3} [CommGroup G] {a b c : G} :
a = b / c ↔ c * a = b
source
theorem eq_sub_iff_add_eq' {G : Type u_3} [AddCommGroup G] {a b c : G} :
a = b - c ↔ c + a = b
source
theorem div_eq_iff_eq_mul' {G : Type u_3} [CommGroup G] {a b c : G} :
a / b = c ↔ a = b * c
source
theorem sub_eq_iff_eq_add' {G : Type u_3} [AddCommGroup G] {a b c : G} :
a - b = c ↔ a = b + c
source
@[simp]
theorem mul_div_cancel_left {G : Type u_3} [CommGroup G] (a b : G) :
a * b / a = b
source
@[simp]
theorem add_sub_cancel_left {G : Type u_3} [AddCommGroup G] (a b : G) :
a + b - a = b
source
@[simp]
theorem mul_div_cancel {G : Type u_3} [CommGroup G] (a b : G) :
a * (b / a) = b
source
@[simp]
theorem add_sub_cancel {G : Type u_3} [AddCommGroup G] (a b : G) :
a + (b - a) = b
source
@[simp]
theorem div_mul_cancel_left {G : Type u_3} [CommGroup G] (a b : G) :
a / (a * b) = b⁻¹
source
@[simp]
theorem sub_add_cancel_left {G : Type u_3} [AddCommGroup G] (a b : G) :
a - (a + b) = -b
source
theorem mul_mul_inv_cancel'_right {G : Type u_3} [CommGroup G] (a b : G) :
a * (b * a⁻¹) = b
source
theorem add_add_neg_cancel'_right {G : Type u_3} [AddCommGroup G] (a b : G) :
a + (b + -a) = b
source
@[simp]
theorem mul_mul_div_cancel {G : Type u_3} [CommGroup G] (a b c : G) :
a * c * (b / c) = a * b
source
@[simp]
theorem add_add_sub_cancel {G : Type u_3} [AddCommGroup G] (a b c : G) :
a + c + (b - c) = a + b
source
@[simp]
theorem div_mul_mul_cancel {G : Type u_3} [CommGroup G] (a b c : G) :
a / c * (b * c) = a * b
source
@[simp]
theorem sub_add_add_cancel {G : Type u_3} [AddCommGroup G] (a b c : G) :
a - c + (b + c) = a + b
source
@[simp]
theorem div_mul_div_cancel' {G : Type u_3} [CommGroup G] (a b c : G) :
a / b * (c / a) = c / b
source
@[simp]
theorem sub_add_sub_cancel' {G : Type u_3} [AddCommGroup G] (a b c : G) :
a - b + (c - a) = c - b
source
@[simp]
theorem mul_div_div_cancel {G : Type u_3} [CommGroup G] (a b c : G) :
a * b / (a / c) = b * c
source
@[simp]
theorem add_sub_sub_cancel {G : Type u_3} [AddCommGroup G] (a b c : G) :
a + b - (a - c) = b + c
source
@[simp]
theorem div_div_div_cancel_left {G : Type u_3} [CommGroup G] (a b c : G) :
c / a / (c / b) = b / a
source
@[simp]
theorem sub_sub_sub_cancel_left {G : Type u_3} [AddCommGroup G] (a b c : G) :
c - a - (c - b) = b - a
source
theorem div_eq_div_iff_mul_eq_mul {G : Type u_3} [CommGroup G] {a b c d : G} :
a / b = c / d ↔ a * d = c * b
source
theorem sub_eq_sub_iff_add_eq_add {G : Type u_3} [AddCommGroup G] {a b c d : G} :
a - b = c - d ↔ a + d = c + b
source
theorem mul_inv_eq_mul_inv_iff_mul_eq_mul {G : Type u_3} [CommGroup G] {a b c d : G} :
a * b⁻¹ = c * d⁻¹ ↔ a * d = c * b
source
theorem add_neg_eq_add_neg_iff_add_eq_add {G : Type u_3} [AddCommGroup G] {a b c d : G} :
a + -b = c + -d ↔ a + d = c + b
source
theorem inv_mul_eq_inv_mul_iff_mul_eq_mul {G : Type u_3} [CommGroup G] {a b c d : G} :
b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b
source
theorem neg_add_eq_neg_add_iff_add_eq_add {G : Type u_3} [AddCommGroup G] {a b c d : G} :
-b + a = -d + c ↔ a + d = c + b
source
theorem div_eq_div_iff_div_eq_div {G : Type u_3} [CommGroup G] {a b c d : G} :
a / b = c / d ↔ a / c = b / d
source
theorem sub_eq_sub_iff_sub_eq_sub {G : Type u_3} [AddCommGroup G] {a b c d : G} :
a - b = c - d ↔ a - c = b - d
source
@[simp]
theorem const_div_involutive {G : Type u_3} [CommGroup G] (a : G) :
Function.Involutive fun (x : G) => a / x
source
@[simp]
theorem const_sub_involutive {G : Type u_3} [AddCommGroup G] (a : G) :
Function.Involutive fun (x : G) => a - x
source
theorem multiplicative_of_symmetric_of_isTotal {α : Type u_1} {β : Type u_2} [Monoid β] (p r : α → α → Prop) [IsTotal α r] (f : α → α → β) (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
source
theorem additive_of_symmetric_of_isTotal {α : Type u_1} {β : Type u_2} [AddMonoid β] (p r : α → α → Prop) [IsTotal α r] (f : α → α → β) (hsymm : Symmetric p) (hf_swap : ∀ {a b : α}, p a b → f a b + f b a = 0) (hadd : ∀ {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
source
theorem multiplicative_of_isTotal {α : Type u_1} {β : Type u_2} [Monoid β] (r : α → α → Prop) [IsTotal α r] (f : α → α → β) (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

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`.

source
theorem additive_of_isTotal {α : Type u_1} {β : Type u_2} [AddMonoid β] (r : α → α → Prop) [IsTotal α r] (f : α → α → β) (p : α → Prop) (hswap : ∀ {a b : α}, p a → p b → f a b + f b a = 0) (hadd : ∀ {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

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`.

source
theorem hom_coe_pow {M : Type u_4} {F : Type u_5} [Monoid F] (c : F → M → M) (h1 : c 1 = id) (hmul : ∀ (f g : F), c (f * g) = c f ∘ c g) (f : F) (n : ℕ) :
c (f ^ n) = (c f)^[n]

An auxiliary lemma that can be used to prove `⇑(f ^ n) = ⇑f^[n]`.

source
theorem hom_coe_nsmul {M : Type u_4} {F : Type u_5} [AddMonoid F] (c : F → M → M) (h1 : c 0 = id) (hadd : ∀ (f g : F), c (f + g) = c f ∘ c g) (f : F) (n : ℕ) :
c (n • f) = (c f)^[n]

### Instances for `grind`. #

source
instance AddCommMonoid.toGrindNatModule (α : Type u_5) [s : AddCommMonoid α] :
Lean.Grind.NatModule α
Equations

- One or more equations did not get rendered due to their size.

source
instance AddCommGroup.toGrindIntModule (α : Type u_5) [s : AddCommGroup α] :
Lean.Grind.IntModule α
Equations

- One or more equations did not get rendered due to their size.

source
instance IsRightCancelAdd.toGrindAddRightCancel (α : Type u_5) [AddSemigroup α] [IsRightCancelAdd α] :
Lean.Grind.AddRightCancel α