mathlib3 documentation

algebra.group.basic

Basic lemmas about semigroups, monoids, and groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

theorem comp_assoc_left {α : Type u_1} (f : α α α) [is_associative α f] (x y : α) :
f x f y = f (f x y)

Composing two associative operations of f : α → α → α on the left is equal to an associative operation on the left.

theorem comp_assoc_right {α : Type u_1} (f : α α α) [is_associative α f] (x y : α) :
((λ (z : α), f z x) λ (z : α), f z y) = λ (z : α), f z (f y x)

Composing two associative operations of f : α → α → α on the right is equal to an associative operation on the right.

@[simp]
theorem comp_add_left {α : Type u_1} [add_semigroup α] (x y : α) :

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

@[simp]
theorem comp_mul_left {α : Type u_1} [semigroup α] (x y : α) :

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

@[simp]
theorem comp_add_right {α : Type u_1} [add_semigroup α] (x y : α) :
((λ (_x : α), _x + x) λ (_x : α), _x + y) = λ (_x : α), _x + (y + x)

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

@[simp]
theorem comp_mul_right {α : Type u_1} [semigroup α] (x y : α) :
((λ (_x : α), _x * x) λ (_x : α), _x * y) = λ (_x : α), _x * (y * x)

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

theorem ite_mul_one {M : Type u} [mul_one_class M] {P : Prop} [decidable P] {a b : M} :
ite P (a * b) 1 = ite P a 1 * ite P b 1
theorem ite_add_zero {M : Type u} [add_zero_class M] {P : Prop} [decidable P] {a b : M} :
ite P (a + b) 0 = ite P a 0 + ite P b 0
theorem ite_zero_add {M : Type u} [add_zero_class M] {P : Prop} [decidable P] {a b : M} :
ite P 0 (a + b) = ite P 0 a + ite P 0 b
theorem ite_one_mul {M : Type u} [mul_one_class M] {P : Prop} [decidable P] {a b : M} :
ite P 1 (a * b) = ite P 1 a * ite P 1 b
theorem eq_zero_iff_eq_zero_of_add_eq_zero {M : Type u} [add_zero_class M] {a b : M} (h : a + b = 0) :
a = 0 b = 0
theorem eq_one_iff_eq_one_of_mul_eq_one {M : Type u} [mul_one_class M] {a b : M} (h : a * b = 1) :
a = 1 b = 1
theorem add_zero_eq_id {M : Type u} [add_zero_class M] :
(λ (_x : M), _x + 0) = id
theorem mul_one_eq_id {M : Type u} [mul_one_class M] :
(λ (_x : M), _x * 1) = id
theorem mul_left_comm {G : Type u_3} [comm_semigroup G] (a b c : G) :
a * (b * c) = b * (a * c)
theorem add_left_comm {G : Type u_3} [add_comm_semigroup G] (a b c : G) :
a + (b + c) = b + (a + c)
theorem mul_right_comm {G : Type u_3} [comm_semigroup G] (a b c : G) :
a * b * c = a * c * b
theorem add_right_comm {G : Type u_3} [add_comm_semigroup G] (a b c : G) :
a + b + c = a + c + b
theorem add_add_add_comm {G : Type u_3} [add_comm_semigroup G] (a b c d : G) :
a + b + (c + d) = a + c + (b + d)
theorem mul_mul_mul_comm {G : Type u_3} [comm_semigroup G] (a b c d : G) :
a * b * (c * d) = a * c * (b * d)
theorem add_rotate {G : Type u_3} [add_comm_semigroup G] (a b c : G) :
a + b + c = b + c + a
theorem mul_rotate {G : Type u_3} [comm_semigroup G] (a b c : G) :
a * b * c = b * c * a
theorem add_rotate' {G : Type u_3} [add_comm_semigroup G] (a b c : G) :
a + (b + c) = b + (c + a)
theorem mul_rotate' {G : Type u_3} [comm_semigroup G] (a b c : G) :
a * (b * c) = b * (c * a)
theorem bit0_add {M : Type u} [add_comm_semigroup M] (a b : M) :
bit0 (a + b) = bit0 a + bit0 b
theorem bit1_add {M : Type u} [add_comm_semigroup M] [has_one M] (a b : M) :
bit1 (a + b) = bit0 a + bit1 b
theorem bit1_add' {M : Type u} [add_comm_semigroup M] [has_one M] (a b : M) :
bit1 (a + b) = bit1 a + bit0 b
@[simp]
theorem bit0_zero {M : Type u} [add_monoid M] :
bit0 0 = 0
@[simp]
theorem bit1_zero {M : Type u} [add_monoid M] [has_one M] :
bit1 0 = 1
theorem inv_unique {M : Type u} [comm_monoid M] {x y z : M} (hy : x * y = 1) (hz : x * z = 1) :
y = z
theorem neg_unique {M : Type u} [add_comm_monoid M] {x y z : M} (hy : x + y = 0) (hz : x + z = 0) :
y = z
@[simp]
theorem add_right_eq_self {M : Type u} [add_left_cancel_monoid M] {a b : M} :
a + b = a b = 0
@[simp]
theorem mul_right_eq_self {M : Type u} [left_cancel_monoid M] {a b : M} :
a * b = a b = 1
@[simp]
theorem self_eq_mul_right {M : Type u} [left_cancel_monoid M] {a b : M} :
a = a * b b = 1
@[simp]
theorem self_eq_add_right {M : Type u} [add_left_cancel_monoid M] {a b : M} :
a = a + b b = 0
theorem add_right_ne_self {M : Type u} [add_left_cancel_monoid M] {a b : M} :
a + b a b 0
theorem mul_right_ne_self {M : Type u} [left_cancel_monoid M] {a b : M} :
a * b a b 1
theorem self_ne_add_right {M : Type u} [add_left_cancel_monoid M] {a b : M} :
a a + b b 0
theorem self_ne_mul_right {M : Type u} [left_cancel_monoid M] {a b : M} :
a a * b b 1
@[simp]
theorem add_left_eq_self {M : Type u} [add_right_cancel_monoid M] {a b : M} :
a + b = b a = 0
@[simp]
theorem mul_left_eq_self {M : Type u} [right_cancel_monoid M] {a b : M} :
a * b = b a = 1
@[simp]
theorem self_eq_add_left {M : Type u} [add_right_cancel_monoid M] {a b : M} :
b = a + b a = 0
@[simp]
theorem self_eq_mul_left {M : Type u} [right_cancel_monoid M] {a b : M} :
b = a * b a = 1
theorem mul_left_ne_self {M : Type u} [right_cancel_monoid M] {a b : M} :
a * b b a 1
theorem add_left_ne_self {M : Type u} [add_right_cancel_monoid M] {a b : M} :
a + b b a 0
theorem self_ne_add_left {M : Type u} [add_right_cancel_monoid M] {a b : M} :
b a + b a 0
theorem self_ne_mul_left {M : Type u} [right_cancel_monoid M] {a b : M} :
b a * b a 1
@[simp]
theorem inv_inj {G : Type u_3} [has_involutive_inv G] {a b : G} :
a⁻¹ = b⁻¹ a = b
@[simp]
theorem neg_inj {G : Type u_3} [has_involutive_neg G] {a b : G} :
-a = -b a = b
theorem inv_eq_iff_eq_inv {G : Type u_3} [has_involutive_inv G] {a b : G} :
a⁻¹ = b a = b⁻¹
theorem neg_eq_iff_eq_neg {G : Type u_3} [has_involutive_neg G] {a b : G} :
-a = b a = -b
theorem left_inverse_neg (G : Type u_3) [has_involutive_neg G] :
function.left_inverse (λ (a : G), -a) (λ (a : G), -a)
theorem left_inverse_inv (G : Type u_3) [has_involutive_inv G] :
function.left_inverse (λ (a : G), a⁻¹) (λ (a : G), a⁻¹)
theorem right_inverse_neg (G : Type u_3) [has_involutive_neg G] :
function.left_inverse (λ (a : G), -a) (λ (a : G), -a)
theorem right_inverse_inv (G : Type u_3) [has_involutive_inv G] :
function.left_inverse (λ (a : G), a⁻¹) (λ (a : G), a⁻¹)
theorem neg_eq_zero_sub {G : Type u_3} [sub_neg_monoid G] (x : G) :
-x = 0 - x
theorem inv_eq_one_div {G : Type u_3} [div_inv_monoid G] (x : G) :
x⁻¹ = 1 / x
theorem add_zero_sub {G : Type u_3} [sub_neg_monoid G] (x y : G) :
x + (0 - y) = x - y
theorem mul_one_div {G : Type u_3} [div_inv_monoid G] (x y : G) :
x * (1 / y) = x / y
theorem mul_div_assoc {G : Type u_3} [div_inv_monoid G] (a b c : G) :
a * b / c = a * (b / c)
theorem add_sub_assoc {G : Type u_3} [sub_neg_monoid G] (a b c : G) :
a + b - c = a + (b - c)
theorem add_sub_assoc' {G : Type u_3} [sub_neg_monoid G] (a b c : G) :
a + (b - c) = a + b - c
theorem mul_div_assoc' {G : Type u_3} [div_inv_monoid G] (a b c : G) :
a * (b / c) = a * b / c
@[simp]
theorem one_div {G : Type u_3} [div_inv_monoid G] (a : G) :
1 / a = a⁻¹
@[simp]
theorem zero_sub {G : Type u_3} [sub_neg_monoid G] (a : G) :
0 - a = -a
theorem mul_div {G : Type u_3} [div_inv_monoid G] (a b c : G) :
a * (b / c) = a * b / c
theorem add_sub {G : Type u_3} [sub_neg_monoid G] (a b c : G) :
a + (b - c) = a + b - c
theorem sub_eq_add_zero_sub {G : Type u_3} [sub_neg_monoid G] (a b : G) :
a - b = a + (0 - b)
theorem div_eq_mul_one_div {G : Type u_3} [div_inv_monoid G] (a b : G) :
a / b = a * (1 / b)
@[simp]
theorem sub_zero {G : Type u_3} [sub_neg_zero_monoid G] (a : G) :
a - 0 = a
@[simp]
theorem div_one {G : Type u_3} [div_inv_one_monoid G] (a : G) :
a / 1 = a
theorem one_div_one {G : Type u_3} [div_inv_one_monoid G] :
1 / 1 = 1
theorem zero_sub_zero {G : Type u_3} [sub_neg_zero_monoid G] :
0 - 0 = 0
theorem inv_eq_of_mul_eq_one_left {α : Type u_1} [division_monoid α] {a b : α} (h : a * b = 1) :
b⁻¹ = a
theorem neg_eq_of_add_eq_zero_left {α : Type u_1} [subtraction_monoid α] {a b : α} (h : a + b = 0) :
-b = a
theorem eq_neg_of_add_eq_zero_left {α : Type u_1} [subtraction_monoid α] {a b : α} (h : a + b = 0) :
a = -b
theorem eq_inv_of_mul_eq_one_left {α : Type u_1} [division_monoid α] {a b : α} (h : a * b = 1) :
a = b⁻¹
theorem eq_neg_of_add_eq_zero_right {α : Type u_1} [subtraction_monoid α] {a b : α} (h : a + b = 0) :
b = -a
theorem eq_inv_of_mul_eq_one_right {α : Type u_1} [division_monoid α] {a b : α} (h : a * b = 1) :
b = a⁻¹
theorem eq_zero_sub_of_add_eq_zero_left {α : Type u_1} [subtraction_monoid α] {a b : α} (h : b + a = 0) :
b = 0 - a
theorem eq_one_div_of_mul_eq_one_left {α : Type u_1} [division_monoid α] {a b : α} (h : b * a = 1) :
b = 1 / a
theorem eq_zero_sub_of_add_eq_zero_right {α : Type u_1} [subtraction_monoid α] {a b : α} (h : a + b = 0) :
b = 0 - a
theorem eq_one_div_of_mul_eq_one_right {α : Type u_1} [division_monoid α] {a b : α} (h : a * b = 1) :
b = 1 / a
theorem eq_of_sub_eq_zero {α : Type u_1} [subtraction_monoid α] {a b : α} (h : a - b = 0) :
a = b
theorem eq_of_div_eq_one {α : Type u_1} [division_monoid α] {a b : α} (h : a / b = 1) :
a = b
theorem div_ne_one_of_ne {α : Type u_1} [division_monoid α] {a b : α} :
a b a / b 1
theorem sub_ne_zero_of_ne {α : Type u_1} [subtraction_monoid α] {a b : α} :
a b a - b 0
theorem zero_sub_add_zero_sub_rev {α : Type u_1} [subtraction_monoid α] (a b : α) :
0 - a + (0 - b) = 0 - (b + a)
theorem one_div_mul_one_div_rev {α : Type u_1} [division_monoid α] (a b : α) :
1 / a * (1 / b) = 1 / (b * a)
theorem neg_sub_left {α : Type u_1} [subtraction_monoid α] (a b : α) :
-a - b = -(b + a)
theorem inv_div_left {α : Type u_1} [division_monoid α] (a b : α) :
a⁻¹ / b = (b * a)⁻¹
@[simp]
theorem neg_sub {α : Type u_1} [subtraction_monoid α] (a b : α) :
-(a - b) = b - a
@[simp]
theorem inv_div {α : Type u_1} [division_monoid α] (a b : α) :
(a / b)⁻¹ = b / a
@[simp]
theorem one_div_div {α : Type u_1} [division_monoid α] (a b : α) :
1 / (a / b) = b / a
@[simp]
theorem zero_sub_sub {α : Type u_1} [subtraction_monoid α] (a b : α) :
0 - (a - b) = b - a
theorem one_div_one_div {α : Type u_1} [division_monoid α] (a : α) :
1 / (1 / a) = a
theorem zero_sub_zero_sub {α : Type u_1} [subtraction_monoid α] (a : α) :
0 - (0 - a) = a
@[simp]
theorem inv_eq_one {α : Type u_1} [division_monoid α] {a : α} :
a⁻¹ = 1 a = 1
@[simp]
theorem neg_eq_zero {α : Type u_1} [subtraction_monoid α] {a : α} :
-a = 0 a = 0
@[simp]
theorem one_eq_inv {α : Type u_1} [division_monoid α] {a : α} :
1 = a⁻¹ a = 1
@[simp]
theorem zero_eq_neg {α : Type u_1} [subtraction_monoid α] {a : α} :
0 = -a a = 0
theorem inv_ne_one {α : Type u_1} [division_monoid α] {a : α} :
a⁻¹ 1 a 1
theorem neg_ne_zero {α : Type u_1} [subtraction_monoid α] {a : α} :
-a 0 a 0
theorem eq_of_zero_sub_eq_zero_sub {α : Type u_1} [subtraction_monoid α] {a b : α} (h : 0 - a = 0 - b) :
a = b
theorem eq_of_one_div_eq_one_div {α : Type u_1} [division_monoid α] {a b : α} (h : 1 / a = 1 / b) :
a = b
theorem div_div_eq_mul_div {α : Type u_1} [division_monoid α] (a b c : α) :
a / (b / c) = a * c / b
theorem sub_sub_eq_add_sub {α : Type u_1} [subtraction_monoid α] (a b c : α) :
a - (b - c) = a + c - b
@[simp]
theorem sub_neg_eq_add {α : Type u_1} [subtraction_monoid α] (a b : α) :
a - -b = a + b
@[simp]
theorem div_inv_eq_mul {α : Type u_1} [division_monoid α] (a b : α) :
a / b⁻¹ = a * b
theorem div_mul_eq_div_div_swap {α : Type u_1} [division_monoid α] (a b c : α) :
a / (b * c) = a / c / b
theorem sub_add_eq_sub_sub_swap {α : Type u_1} [subtraction_monoid α] (a b c : α) :
a - (b + c) = a - c - b
theorem bit0_neg {α : Type u_1} [subtraction_monoid α] (a : α) :
bit0 (-a) = -bit0 a
theorem mul_inv {α : Type u_1} [division_comm_monoid α] (a b : α) :
(a * b)⁻¹ = a⁻¹ * b⁻¹
theorem neg_add {α : Type u_1} [subtraction_comm_monoid α] (a b : α) :
-(a + b) = -a + -b
theorem inv_div' {α : Type u_1} [division_comm_monoid α] (a b : α) :
(a / b)⁻¹ = a⁻¹ / b⁻¹
theorem neg_sub' {α : Type u_1} [subtraction_comm_monoid α] (a b : α) :
-(a - b) = -a - -b
theorem sub_eq_neg_add {α : Type u_1} [subtraction_comm_monoid α] (a b : α) :
a - b = -b + a
theorem div_eq_inv_mul {α : Type u_1} [division_comm_monoid α] (a b : α) :
a / b = b⁻¹ * a
theorem neg_add_eq_sub {α : Type u_1} [subtraction_comm_monoid α] (a b : α) :
-a + b = b - a
theorem inv_mul_eq_div {α : Type u_1} [division_comm_monoid α] (a b : α) :
a⁻¹ * b = b / a
theorem inv_mul' {α : Type u_1} [division_comm_monoid α] (a b : α) :
(a * b)⁻¹ = a⁻¹ / b
theorem neg_add' {α : Type u_1} [subtraction_comm_monoid α] (a b : α) :
-(a + b) = -a - b
@[simp]
theorem inv_div_inv {α : Type u_1} [division_comm_monoid α] (a b : α) :
a⁻¹ / b⁻¹ = b / a
@[simp]
theorem neg_sub_neg {α : Type u_1} [subtraction_comm_monoid α] (a b : α) :
-a - -b = b - a
theorem neg_neg_sub_neg {α : Type u_1} [subtraction_comm_monoid α] (a b : α) :
-(-a - -b) = a - b
theorem inv_inv_div_inv {α : Type u_1} [division_comm_monoid α] (a b : α) :
(a⁻¹ / b⁻¹)⁻¹ = a / b
theorem one_div_mul_one_div {α : Type u_1} [division_comm_monoid α] (a b : α) :
1 / a * (1 / b) = 1 / (a * b)
theorem zero_sub_add_zero_sub {α : Type u_1} [subtraction_comm_monoid α] (a b : α) :
0 - a + (0 - b) = 0 - (a + b)
theorem sub_right_comm {α : Type u_1} [subtraction_comm_monoid α] (a b c : α) :
a - b - c = a - c - b
theorem div_right_comm {α : Type u_1} [division_comm_monoid α] (a b c : α) :
a / b / c = a / c / b
theorem sub_sub {α : Type u_1} [subtraction_comm_monoid α] (a b c : α) :
a - b - c = a - (b + c)
theorem div_div {α : Type u_1} [division_comm_monoid α] (a b c : α) :
a / b / c = a / (b * c)
theorem div_mul {α : Type u_1} [division_comm_monoid α] (a b c : α) :
a / b * c = a / (b / c)
theorem sub_add {α : Type u_1} [subtraction_comm_monoid α] (a b c : α) :
a - b + c = a - (b - c)
theorem add_sub_left_comm {α : Type u_1} [subtraction_comm_monoid α] (a b c : α) :
a + (b - c) = b + (a - c)
theorem mul_div_left_comm {α : Type u_1} [division_comm_monoid α] (a b c : α) :
a * (b / c) = b * (a / c)
theorem mul_div_right_comm {α : Type u_1} [division_comm_monoid α] (a b c : α) :
a * b / c = a / c * b
theorem add_sub_right_comm {α : Type u_1} [subtraction_comm_monoid α] (a b c : α) :
a + b - c = a - c + b
theorem div_mul_eq_div_div {α : Type u_1} [division_comm_monoid α] (a b c : α) :
a / (b * c) = a / b / c
theorem sub_add_eq_sub_sub {α : Type u_1} [subtraction_comm_monoid α] (a b c : α) :
a - (b + c) = a - b - c
theorem div_mul_eq_mul_div {α : Type u_1} [division_comm_monoid α] (a b c : α) :
a / b * c = a * c / b
theorem sub_add_eq_add_sub {α : Type u_1} [subtraction_comm_monoid α] (a b c : α) :
a - b + c = a + c - b
theorem mul_comm_div {α : Type u_1} [division_comm_monoid α] (a b c : α) :
a / b * c = a * (c / b)
theorem add_comm_sub {α : Type u_1} [subtraction_comm_monoid α] (a b c : α) :
a - b + c = a + (c - b)
theorem sub_add_comm {α : Type u_1} [subtraction_comm_monoid α] (a b c : α) :
a - b + c = c - b + a
theorem div_mul_comm {α : Type u_1} [division_comm_monoid α] (a b c : α) :
a / b * c = c / b * a
theorem sub_add_eq_sub_add_zero_sub {α : Type u_1} [subtraction_comm_monoid α] (a b c : α) :
a - (b + c) = a - b + (0 - c)
theorem div_mul_eq_div_mul_one_div {α : Type u_1} [division_comm_monoid α] (a b c : α) :
a / (b * c) = a / b * (1 / c)
theorem sub_sub_sub_eq {α : Type u_1} [subtraction_comm_monoid α] (a b c d : α) :
a - b - (c - d) = a + d - (b + c)
theorem div_div_div_eq {α : Type u_1} [division_comm_monoid α] (a b c d : α) :
a / b / (c / d) = a * d / (b * c)
theorem div_div_div_comm {α : Type u_1} [division_comm_monoid α] (a b c d : α) :
a / b / (c / d) = a / c / (b / d)
theorem sub_sub_sub_comm {α : Type u_1} [subtraction_comm_monoid α] (a b c d : α) :
a - b - (c - d) = a - c - (b - d)
theorem div_mul_div_comm {α : Type u_1} [division_comm_monoid α] (a b c d : α) :
a / b * (c / d) = a * c / (b * d)
theorem sub_add_sub_comm {α : Type u_1} [subtraction_comm_monoid α] (a b c d : α) :
a - b + (c - d) = a + c - (b + d)
theorem mul_div_mul_comm {α : Type u_1} [division_comm_monoid α] (a b c d : α) :
a * b / (c * d) = a / c * (b / d)
theorem add_sub_add_comm {α : Type u_1} [subtraction_comm_monoid α] (a b c d : α) :
a + b - (c + d) = a - c + (b - d)
@[simp]
theorem sub_eq_neg_self {G : Type u_3} [add_group G] {a b : G} :
a - b = -b a = 0
@[simp]
theorem div_eq_inv_self {G : Type u_3} [group G] {a b : G} :
a / b = b⁻¹ a = 1
theorem mul_left_surjective {G : Type u_3} [group G] (a : G) :
theorem add_right_surjective {G : Type u_3} [add_group G] (a : G) :
function.surjective (λ (x : G), x + a)
theorem mul_right_surjective {G : Type u_3} [group G] (a : G) :
function.surjective (λ (x : G), x * a)
theorem eq_add_neg_of_add_eq {G : Type u_3} [add_group G] {a b c : G} (h : a + c = b) :
a = b + -c
theorem eq_mul_inv_of_mul_eq {G : Type u_3} [group G] {a b c : G} (h : a * c = b) :
a = b * c⁻¹
theorem eq_neg_add_of_add_eq {G : Type u_3} [add_group G] {a b c : G} (h : b + a = c) :
a = -b + c
theorem eq_inv_mul_of_mul_eq {G : Type u_3} [group G] {a b c : G} (h : b * a = c) :
a = b⁻¹ * c
theorem inv_mul_eq_of_eq_mul {G : Type u_3} [group G] {a b c : G} (h : b = a * c) :
a⁻¹ * b = c
theorem neg_add_eq_of_eq_add {G : Type u_3} [add_group G] {a b c : G} (h : b = a + c) :
-a + b = c
theorem add_neg_eq_of_eq_add {G : Type u_3} [add_group G] {a b c : G} (h : a = c + b) :
a + -b = c
theorem mul_inv_eq_of_eq_mul {G : Type u_3} [group G] {a b c : G} (h : a = c * b) :
a * b⁻¹ = c
theorem eq_add_of_add_neg_eq {G : Type u_3} [add_group G] {a b c : G} (h : a + -c = b) :
a = b + c
theorem eq_mul_of_mul_inv_eq {G : Type u_3} [group G] {a b c : G} (h : a * c⁻¹ = b) :
a = b * c
theorem eq_mul_of_inv_mul_eq {G : Type u_3} [group G] {a b c : G} (h : b⁻¹ * a = c) :
a = b * c
theorem eq_add_of_neg_add_eq {G : Type u_3} [add_group G] {a b c : G} (h : -b + a = c) :
a = b + c
theorem mul_eq_of_eq_inv_mul {G : Type u_3} [group G] {a b c : G} (h : b = a⁻¹ * c) :
a * b = c
theorem add_eq_of_eq_neg_add {G : Type u_3} [add_group G] {a b c : G} (h : b = -a + c) :
a + b = c
theorem mul_eq_of_eq_mul_inv {G : Type u_3} [group G] {a b c : G} (h : a = c * b⁻¹) :
a * b = c
theorem add_eq_of_eq_add_neg {G : Type u_3} [add_group G] {a b c : G} (h : a = c + -b) :
a + b = c
theorem mul_eq_one_iff_eq_inv {G : Type u_3} [group G] {a b : G} :
a * b = 1 a = b⁻¹
theorem add_eq_zero_iff_eq_neg {G : Type u_3} [add_group G] {a b : G} :
a + b = 0 a = -b
theorem mul_eq_one_iff_inv_eq {G : Type u_3} [group G] {a b : G} :
a * b = 1 a⁻¹ = b
theorem add_eq_zero_iff_neg_eq {G : Type u_3} [add_group G] {a b : G} :
a + b = 0 -a = b
theorem eq_inv_iff_mul_eq_one {G : Type u_3} [group G] {a b : G} :
a = b⁻¹ a * b = 1
theorem eq_neg_iff_add_eq_zero {G : Type u_3} [add_group G] {a b : G} :
a = -b a + b = 0
theorem neg_eq_iff_add_eq_zero {G : Type u_3} [add_group G] {a b : G} :
-a = b a + b = 0
theorem inv_eq_iff_mul_eq_one {G : Type u_3} [group G] {a b : G} :
a⁻¹ = b a * b = 1
theorem eq_add_neg_iff_add_eq {G : Type u_3} [add_group G] {a b c : G} :
a = b + -c a + c = b
theorem eq_mul_inv_iff_mul_eq {G : Type u_3} [group G] {a b c : G} :
a = b * c⁻¹ a * c = b
theorem eq_inv_mul_iff_mul_eq {G : Type u_3} [group G] {a b c : G} :
a = b⁻¹ * c b * a = c
theorem eq_neg_add_iff_add_eq {G : Type u_3} [add_group G] {a b c : G} :
a = -b + c b + a = c
theorem neg_add_eq_iff_eq_add {G : Type u_3} [add_group G] {a b c : G} :
-a + b = c b = a + c
theorem inv_mul_eq_iff_eq_mul {G : Type u_3} [group G] {a b c : G} :
a⁻¹ * b = c b = a * c
theorem add_neg_eq_iff_eq_add {G : Type u_3} [add_group G] {a b c : G} :
a + -b = c a = c + b
theorem mul_inv_eq_iff_eq_mul {G : Type u_3} [group G] {a b c : G} :
a * b⁻¹ = c a = c * b
theorem mul_inv_eq_one {G : Type u_3} [group G] {a b : G} :
a * b⁻¹ = 1 a = b
theorem add_neg_eq_zero {G : Type u_3} [add_group G] {a b : G} :
a + -b = 0 a = b
theorem inv_mul_eq_one {G : Type u_3} [group G] {a b : G} :
a⁻¹ * b = 1 a = b
theorem neg_add_eq_zero {G : Type u_3} [add_group G] {a b : G} :
-a + b = 0 a = b
theorem sub_left_injective {G : Type u_3} [add_group G] {b : G} :
function.injective (λ (a : G), a - b)
theorem div_left_injective {G : Type u_3} [group G] {b : G} :
function.injective (λ (a : G), a / b)
theorem div_right_injective {G : Type u_3} [group G] {b : G} :
function.injective (λ (a : G), b / a)
theorem sub_right_injective {G : Type u_3} [add_group G] {b : G} :
function.injective (λ (a : G), b - a)
@[simp]
theorem sub_add_cancel {G : Type u_3} [add_group G] (a b : G) :
a - b + b = a
@[simp]
theorem div_mul_cancel' {G : Type u_3} [group G] (a b : G) :
a / b * b = a
@[simp]
theorem div_self' {G : Type u_3} [group G] (a : G) :
a / a = 1
@[simp]
theorem sub_self {G : Type u_3} [add_group G] (a : G) :
a - a = 0
@[simp]
theorem mul_div_cancel'' {G : Type u_3} [group G] (a b : G) :
a * b / b = a
@[simp]
theorem add_sub_cancel {G : Type u_3} [add_group G] (a b : G) :
a + b - b = a
@[simp]
theorem sub_add_cancel'' {G : Type u_3} [add_group G] (a b : G) :
a - (b + a) = -b
@[simp]
theorem div_mul_cancel''' {G : Type u_3} [group G] (a b : G) :
a / (b * a) = b⁻¹
@[simp]
theorem mul_div_mul_right_eq_div {G : Type u_3} [group G] (a b c : G) :
a * c / (b * c) = a / b
@[simp]
theorem add_sub_add_right_eq_sub {G : Type u_3} [add_group G] (a b c : G) :
a + c - (b + c) = a - b
theorem eq_sub_of_add_eq {G : Type u_3} [add_group G] {a b c : G} (h : a + c = b) :
a = b - c
theorem eq_div_of_mul_eq' {G : Type u_3} [group G] {a b c : G} (h : a * c = b) :
a = b / c
theorem div_eq_of_eq_mul'' {G : Type u_3} [group G] {a b c : G} (h : a = c * b) :
a / b = c
theorem sub_eq_of_eq_add {G : Type u_3} [add_group G] {a b c : G} (h : a = c + b) :
a - b = c
theorem eq_mul_of_div_eq {G : Type u_3} [group G] {a b c : G} (h : a / c = b) :
a = b * c
theorem eq_add_of_sub_eq {G : Type u_3} [add_group G] {a b c : G} (h : a - c = b) :
a = b + c
theorem mul_eq_of_eq_div {G : Type u_3} [group G] {a b c : G} (h : a = c / b) :
a * b = c
theorem add_eq_of_eq_sub {G : Type u_3} [add_group G] {a b c : G} (h : a = c - b) :
a + b = c
@[simp]
theorem div_right_inj {G : Type u_3} [group G] {a b c : G} :
a / b = a / c b = c
@[simp]
theorem sub_right_inj {G : Type u_3} [add_group G] {a b c : G} :
a - b = a - c b = c
@[simp]
theorem div_left_inj {G : Type u_3} [group G] {a b c : G} :
b / a = c / a b = c
@[simp]
theorem sub_left_inj {G : Type u_3} [add_group G] {a b c : G} :
b - a = c - a b = c
@[simp]
theorem div_mul_div_cancel' {G : Type u_3} [group G] (a b c : G) :
a / b * (b / c) = a / c
@[simp]
theorem sub_add_sub_cancel {G : Type u_3} [add_group G] (a b c : G) :
a - b + (b - c) = a - c
@[simp]
theorem div_div_div_cancel_right' {G : Type u_3} [group G] (a b c : G) :
a / c / (b / c) = a / b
@[simp]
theorem sub_sub_sub_cancel_right {G : Type u_3} [add_group G] (a b c : G) :
a - c - (b - c) = a - b
theorem div_eq_one {G : Type u_3} [group G] {a b : G} :
a / b = 1 a = b
theorem sub_eq_zero {G : Type u_3} [add_group G] {a b : G} :
a - b = 0 a = b
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.

theorem sub_eq_zero_of_eq {G : Type u_3} [add_group G] {a b : G} :
a = b a - b = 0

Alias of the reverse direction of sub_eq_zero.

theorem sub_ne_zero {G : Type u_3} [add_group G] {a b : G} :
a - b 0 a b
theorem div_ne_one {G : Type u_3} [group G] {a b : G} :
a / b 1 a b
@[simp]
theorem sub_eq_self {G : Type u_3} [add_group G] {a b : G} :
a - b = a b = 0
@[simp]
theorem div_eq_self {G : Type u_3} [group G] {a b : G} :
a / b = a b = 1
theorem eq_div_iff_mul_eq' {G : Type u_3} [group G] {a b c : G} :
a = b / c a * c = b
theorem eq_sub_iff_add_eq {G : Type u_3} [add_group G] {a b c : G} :
a = b - c a + c = b
theorem sub_eq_iff_eq_add {G : Type u_3} [add_group G] {a b c : G} :
a - b = c a = c + b
theorem div_eq_iff_eq_mul {G : Type u_3} [group G] {a b c : G} :
a / b = c a = c * b
theorem eq_iff_eq_of_sub_eq_sub {G : Type u_3} [add_group G] {a b c d : G} (H : a - b = c - d) :
a = b c = d
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
theorem left_inverse_sub_add_left {G : Type u_3} [add_group G] (c : G) :
function.left_inverse (λ (x : G), x - c) (λ (x : G), x + c)
theorem left_inverse_div_mul_left {G : Type u_3} [group G] (c : G) :
function.left_inverse (λ (x : G), x / c) (λ (x : G), x * c)
theorem left_inverse_add_left_sub {G : Type u_3} [add_group G] (c : G) :
function.left_inverse (λ (x : G), x + c) (λ (x : G), x - c)
theorem left_inverse_mul_left_div {G : Type u_3} [group G] (c : G) :
function.left_inverse (λ (x : G), x * c) (λ (x : G), x / c)
theorem left_inverse_add_right_neg_add {G : Type u_3} [add_group G] (c : G) :
function.left_inverse (λ (x : G), c + x) (λ (x : G), -c + x)
theorem left_inverse_mul_right_inv_mul {G : Type u_3} [group G] (c : G) :
function.left_inverse (λ (x : G), c * x) (λ (x : G), c⁻¹ * x)
theorem left_inverse_neg_add_add_right {G : Type u_3} [add_group G] (c : G) :
function.left_inverse (λ (x : G), -c + x) (λ (x : G), c + x)
theorem left_inverse_inv_mul_mul_right {G : Type u_3} [group G] (c : G) :
function.left_inverse (λ (x : G), c⁻¹ * x) (λ (x : G), c * x)
theorem exists_npow_eq_one_of_zpow_eq_one {G : Type u_3} [group G] {n : } (hn : n 0) {x : G} (h : x ^ n = 1) :
(n : ), 0 < n x ^ n = 1
theorem exists_nsmul_eq_zero_of_zsmul_eq_zero {G : Type u_3} [add_group G] {n : } (hn : n 0) {x : G} (h : n x = 0) :
(n : ), 0 < n n x = 0
theorem div_eq_of_eq_mul' {G : Type u_3} [comm_group G] {a b c : G} (h : a = b * c) :
a / b = c
theorem sub_eq_of_eq_add' {G : Type u_3} [add_comm_group G] {a b c : G} (h : a = b + c) :
a - b = c
@[simp]
theorem add_sub_add_left_eq_sub {G : Type u_3} [add_comm_group G] (a b c : G) :
c + a - (c + b) = a - b
@[simp]
theorem mul_div_mul_left_eq_div {G : Type u_3} [comm_group G] (a b c : G) :
c * a / (c * b) = a / b
theorem eq_div_of_mul_eq'' {G : Type u_3} [comm_group G] {a b c : G} (h : c * a = b) :
a = b / c
theorem eq_sub_of_add_eq' {G : Type u_3} [add_comm_group G] {a b c : G} (h : c + a = b) :
a = b - c
theorem eq_mul_of_div_eq' {G : Type u_3} [comm_group G] {a b c : G} (h : a / b = c) :
a = b * c
theorem eq_add_of_sub_eq' {G : Type u_3} [add_comm_group G] {a b c : G} (h : a - b = c) :
a = b + c
theorem add_eq_of_eq_sub' {G : Type u_3} [add_comm_group G] {a b c : G} (h : b = c - a) :
a + b = c
theorem mul_eq_of_eq_div' {G : Type u_3} [comm_group G] {a b c : G} (h : b = c / a) :
a * b = c
theorem sub_sub_self {G : Type u_3} [add_comm_group G] (a b : G) :
a - (a - b) = b
theorem div_div_self' {G : Type u_3} [comm_group G] (a b : G) :
a / (a / b) = b
theorem div_eq_div_mul_div {G : Type u_3} [comm_group G] (a b c : G) :
a / b = c / b * (a / c)
theorem sub_eq_sub_add_sub {G : Type u_3} [add_comm_group G] (a b c : G) :
a - b = c - b + (a - c)
@[simp]
theorem sub_sub_cancel {G : Type u_3} [add_comm_group G] (a b : G) :
a - (a - b) = b
@[simp]
theorem div_div_cancel {G : Type u_3} [comm_group G] (a b : G) :
a / (a / b) = b
@[simp]
theorem div_div_cancel_left {G : Type u_3} [comm_group G] (a b : G) :
a / b / a = b⁻¹
@[simp]
theorem sub_sub_cancel_left {G : Type u_3} [add_comm_group G] (a b : G) :
a - b - a = -b
theorem eq_div_iff_mul_eq'' {G : Type u_3} [comm_group G] {a b c : G} :
a = b / c c * a = b
theorem eq_sub_iff_add_eq' {G : Type u_3} [add_comm_group G] {a b c : G} :
a = b - c c + a = b
theorem div_eq_iff_eq_mul' {G : Type u_3} [comm_group G] {a b c : G} :
a / b = c a = b * c
theorem sub_eq_iff_eq_add' {G : Type u_3} [add_comm_group G] {a b c : G} :
a - b = c a = b + c
@[simp]
theorem add_sub_cancel' {G : Type u_3} [add_comm_group G] (a b : G) :
a + b - a = b
@[simp]
theorem mul_div_cancel''' {G : Type u_3} [comm_group G] (a b : G) :
a * b / a = b
@[simp]
theorem add_sub_cancel'_right {G : Type u_3} [add_comm_group G] (a b : G) :
a + (b - a) = b
@[simp]
theorem mul_div_cancel'_right {G : Type u_3} [comm_group G] (a b : G) :
a * (b / a) = b
@[simp]
theorem sub_add_cancel' {G : Type u_3} [add_comm_group G] (a b : G) :
a - (a + b) = -b
@[simp]
theorem div_mul_cancel'' {G : Type u_3} [comm_group G] (a b : G) :
a / (a * b) = b⁻¹
theorem mul_mul_inv_cancel'_right {G : Type u_3} [comm_group G] (a b : G) :
a * (b * a⁻¹) = b
theorem add_add_neg_cancel'_right {G : Type u_3} [add_comm_group G] (a b : G) :
a + (b + -a) = b
@[simp]
theorem add_add_sub_cancel {G : Type u_3} [add_comm_group G] (a b c : G) :
a + c + (b - c) = a + b
@[simp]
theorem mul_mul_div_cancel {G : Type u_3} [comm_group G] (a b c : G) :
a * c * (b / c) = a * b
@[simp]
theorem sub_add_add_cancel {G : Type u_3} [add_comm_group G] (a b c : G) :
a - c + (b + c) = a + b
@[simp]
theorem div_mul_mul_cancel {G : Type u_3} [comm_group G] (a b c : G) :
a / c * (b * c) = a * b
@[simp]
theorem div_mul_div_cancel'' {G : Type u_3} [comm_group G] (a b c : G) :
a / b * (c / a) = c / b
@[simp]
theorem sub_add_sub_cancel' {G : Type u_3} [add_comm_group G] (a b c : G) :
a - b + (c - a) = c - b
@[simp]
theorem add_sub_sub_cancel {G : Type u_3} [add_comm_group G] (a b c : G) :
a + b - (a - c) = b + c
@[simp]
theorem mul_div_div_cancel {G : Type u_3} [comm_group G] (a b c : G) :
a * b / (a / c) = b * c
@[simp]
theorem sub_sub_sub_cancel_left {G : Type u_3} [add_comm_group G] (a b c : G) :
c - a - (c - b) = b - a
@[simp]
theorem div_div_div_cancel_left {G : Type u_3} [comm_group G] (a b c : G) :
c / a / (c / b) = b / a
theorem sub_eq_sub_iff_add_eq_add {G : Type u_3} [add_comm_group G] {a b c d : G} :
a - b = c - d a + d = c + b
theorem div_eq_div_iff_mul_eq_mul {G : Type u_3} [comm_group G] {a b c d : G} :
a / b = c / d a * d = c * b
theorem sub_eq_sub_iff_sub_eq_sub {G : Type u_3} [add_comm_group G] {a b c d : G} :
a - b = c - d a - c = b - d
theorem div_eq_div_iff_div_eq_div {G : Type u_3} [comm_group G] {a b c d : G} :
a / b = c / d a / c = b / d
theorem bit0_sub {M : Type u} [subtraction_comm_monoid M] (a b : M) :
bit0 (a - b) = bit0 a - bit0 b
theorem bit1_sub {M : Type u} [subtraction_comm_monoid M] [has_one M] (a b : M) :
bit1 (a - b) = bit1 a - bit0 b
theorem multiplicative_of_symmetric_of_is_total {α : Type u_1} {β : Type u_2} [monoid β] (p r : α α Prop) [is_total α 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
theorem additive_of_symmetric_of_is_total {α : Type u_1} {β : Type u_2} [add_monoid β] (p r : α α Prop) [is_total α r] (f : α α β) (hsymm : symmetric p) (hf_swap : {a b : α}, p a b f a b + f b a = 0) (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
theorem multiplicative_of_is_total {α : Type u_1} {β : Type u_2} [monoid β] (r : α α Prop) [is_total α 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.

theorem additive_of_is_total {α : Type u_1} {β : Type u_2} [add_monoid β] (r : α α Prop) [is_total α r] (f : α α β) (p : α Prop) (hswap : {a b : α}, p a p b f a b + f b a = 0) (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 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.