mathlib documentation

algebra.group.basic

theorem ite_mul_one {M : Type u} [monoid 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_monoid M] {P : Prop} [decidable P] {a b : M} :
ite P (a + b) 0 = ite P a 0 + ite P b 0

theorem mul_left_comm {G : Type u} [comm_semigroup G] (a b c : G) :
a * b * c = b * a * c

theorem add_left_comm {G : Type u} [add_comm_semigroup G] (a b c : G) :
a + (b + c) = b + (a + c)

theorem mul_right_comm {G : Type u} [comm_semigroup G] (a b c : G) :
(a * b) * c = (a * c) * b

theorem add_right_comm {G : Type u} [add_comm_semigroup G] (a b c : G) :
a + b + c = a + c + b

theorem add_add_add_comm {G : Type u} [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} [comm_semigroup G] (a b c d : G) :
(a * b) * c * d = (a * c) * b * d

@[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} :
x * y = 1x * z = 1y = z

theorem neg_unique {M : Type u} [add_comm_monoid M] {x y z : M} :
x + y = 0x + z = 0y = z

theorem eq_one_of_mul_self_left_cancel {M : Type u} [left_cancel_monoid M] {a : M} :
a * a = aa = 1

theorem eq_zero_of_add_self_left_cancel {M : Type u} [add_left_cancel_monoid M] {a : M} :
a + a = aa = 0

theorem eq_zero_of_left_cancel_add_self {M : Type u} [add_left_cancel_monoid M] {a : M} :
a = a + aa = 0

theorem eq_one_of_left_cancel_mul_self {M : Type u} [left_cancel_monoid M] {a : M} :
a = a * aa = 1

theorem eq_zero_of_add_self_right_cancel {M : Type u} [add_right_cancel_monoid M] {a : M} :
a + a = aa = 0

theorem eq_one_of_mul_self_right_cancel {M : Type u} [right_cancel_monoid M] {a : M} :
a * a = aa = 1

theorem eq_one_of_right_cancel_mul_self {M : Type u} [right_cancel_monoid M] {a : M} :
a = a * aa = 1

theorem eq_zero_of_right_cancel_add_self {M : Type u} [add_right_cancel_monoid M] {a : M} :
a = a + aa = 0

@[simp]
theorem neg_add_cancel_right {G : Type u} [add_group G] (a b : G) :
a + -b + b = a

@[simp]
theorem inv_mul_cancel_right {G : Type u} [group G] (a b : G) :
(a * b⁻¹) * b = a

@[simp]
theorem one_inv {G : Type u} [group G] :
1⁻¹ = 1

@[simp]
theorem neg_zero {G : Type u} [add_group G] :
-0 = 0

theorem left_inverse_neg (G : Type u_1) [add_group G] :
function.left_inverse (λ (a : G), -a) (λ (a : G), -a)

theorem left_inverse_inv (G : Type u_1) [group G] :
function.left_inverse (λ (a : G), a⁻¹) (λ (a : G), a⁻¹)

@[simp]
theorem inv_involutive {G : Type u} [group G] :

@[simp]

@[simp]
theorem inv_inj {G : Type u} [group G] {a b : G} :
a⁻¹ = b⁻¹ a = b

@[simp]
theorem neg_inj {G : Type u} [add_group G] {a b : G} :
-a = -b a = b

@[simp]
theorem mul_inv_cancel_left {G : Type u} [group G] (a b : G) :
a * a⁻¹ * b = b

@[simp]
theorem add_neg_cancel_left {G : Type u} [add_group G] (a b : G) :
a + (-a + b) = b

theorem mul_left_surjective {G : Type u} [group G] (a : G) :

theorem add_left_surjective {G : Type u} [add_group G] (a : G) :

theorem add_right_surjective {G : Type u} [add_group G] (a : G) :
function.surjective (λ (x : G), x + a)

theorem mul_right_surjective {G : Type u} [group G] (a : G) :
function.surjective (λ (x : G), x * a)

@[simp]
theorem mul_inv_rev {G : Type u} [group G] (a b : G) :
(a * b)⁻¹ = b⁻¹ * a⁻¹

@[simp]
theorem neg_add_rev {G : Type u} [add_group G] (a b : G) :
-(a + b) = -b + -a

theorem eq_inv_of_eq_inv {G : Type u} [group G] {a b : G} :
a = b⁻¹b = a⁻¹

theorem eq_neg_of_eq_neg {G : Type u} [add_group G] {a b : G} :
a = -bb = -a

theorem eq_inv_of_mul_eq_one {G : Type u} [group G] {a b : G} :
a * b = 1a = b⁻¹

theorem eq_neg_of_add_eq_zero {G : Type u} [add_group G] {a b : G} :
a + b = 0a = -b

theorem eq_add_neg_of_add_eq {G : Type u} [add_group G] {a b c : G} :
a + c = ba = b + -c

theorem eq_mul_inv_of_mul_eq {G : Type u} [group G] {a b c : G} :
a * c = ba = b * c⁻¹

theorem eq_neg_add_of_add_eq {G : Type u} [add_group G] {a b c : G} :
b + a = ca = -b + c

theorem eq_inv_mul_of_mul_eq {G : Type u} [group G] {a b c : G} :
b * a = ca = b⁻¹ * c

theorem inv_mul_eq_of_eq_mul {G : Type u} [group G] {a b c : G} :
b = a * ca⁻¹ * b = c

theorem neg_add_eq_of_eq_add {G : Type u} [add_group G] {a b c : G} :
b = a + c-a + b = c

theorem add_neg_eq_of_eq_add {G : Type u} [add_group G] {a b c : G} :
a = c + ba + -b = c

theorem mul_inv_eq_of_eq_mul {G : Type u} [group G] {a b c : G} :
a = c * ba * b⁻¹ = c

theorem eq_add_of_add_neg_eq {G : Type u} [add_group G] {a b c : G} :
a + -c = ba = b + c

theorem eq_mul_of_mul_inv_eq {G : Type u} [group G] {a b c : G} :
a * c⁻¹ = ba = b * c

theorem eq_mul_of_inv_mul_eq {G : Type u} [group G] {a b c : G} :
b⁻¹ * a = ca = b * c

theorem eq_add_of_neg_add_eq {G : Type u} [add_group G] {a b c : G} :
-b + a = ca = b + c

theorem mul_eq_of_eq_inv_mul {G : Type u} [group G] {a b c : G} :
b = a⁻¹ * ca * b = c

theorem add_eq_of_eq_neg_add {G : Type u} [add_group G] {a b c : G} :
b = -a + ca + b = c

theorem mul_eq_of_eq_mul_inv {G : Type u} [group G] {a b c : G} :
a = c * b⁻¹a * b = c

theorem add_eq_of_eq_add_neg {G : Type u} [add_group G] {a b c : G} :
a = c + -ba + b = c

theorem mul_self_iff_eq_one {G : Type u} [group G] {a : G} :
a * a = a a = 1

theorem add_self_iff_eq_zero {G : Type u} [add_group G] {a : G} :
a + a = a a = 0

@[simp]
theorem inv_eq_one {G : Type u} [group G] {a : G} :
a⁻¹ = 1 a = 1

@[simp]
theorem neg_eq_zero {G : Type u} [add_group G] {a : G} :
-a = 0 a = 0

theorem inv_ne_one {G : Type u} [group G] {a : G} :
a⁻¹ 1 a 1

theorem neg_ne_zero {G : Type u} [add_group G] {a : G} :
-a 0 a 0

theorem eq_inv_iff_eq_inv {G : Type u} [group G] {a b : G} :
a = b⁻¹ b = a⁻¹

theorem eq_neg_iff_eq_neg {G : Type u} [add_group G] {a b : G} :
a = -b b = -a

theorem neg_eq_iff_neg_eq {G : Type u} [add_group G] {a b : G} :
-a = b -b = a

theorem inv_eq_iff_inv_eq {G : Type u} [group G] {a b : G} :
a⁻¹ = b b⁻¹ = a

theorem mul_eq_one_iff_eq_inv {G : Type u} [group G] {a b : G} :
a * b = 1 a = b⁻¹

theorem add_eq_zero_iff_eq_neg {G : Type u} [add_group G] {a b : G} :
a + b = 0 a = -b

theorem mul_eq_one_iff_inv_eq {G : Type u} [group G] {a b : G} :
a * b = 1 a⁻¹ = b

theorem add_eq_zero_iff_neg_eq {G : Type u} [add_group G] {a b : G} :
a + b = 0 -a = b

theorem eq_inv_iff_mul_eq_one {G : Type u} [group G] {a b : G} :
a = b⁻¹ a * b = 1

theorem eq_neg_iff_add_eq_zero {G : Type u} [add_group G] {a b : G} :
a = -b a + b = 0

theorem neg_eq_iff_add_eq_zero {G : Type u} [add_group G] {a b : G} :
-a = b a + b = 0

theorem inv_eq_iff_mul_eq_one {G : Type u} [group G] {a b : G} :
a⁻¹ = b a * b = 1

theorem eq_add_neg_iff_add_eq {G : Type u} [add_group G] {a b c : G} :
a = b + -c a + c = b

theorem eq_mul_inv_iff_mul_eq {G : Type u} [group G] {a b c : G} :
a = b * c⁻¹ a * c = b

theorem eq_inv_mul_iff_mul_eq {G : Type u} [group G] {a b c : G} :
a = b⁻¹ * c b * a = c

theorem eq_neg_add_iff_add_eq {G : Type u} [add_group G] {a b c : G} :
a = -b + c b + a = c

theorem neg_add_eq_iff_eq_add {G : Type u} [add_group G] {a b c : G} :
-a + b = c b = a + c

theorem inv_mul_eq_iff_eq_mul {G : Type u} [group G] {a b c : G} :
a⁻¹ * b = c b = a * c

theorem add_neg_eq_iff_eq_add {G : Type u} [add_group G] {a b c : G} :
a + -b = c a = c + b

theorem mul_inv_eq_iff_eq_mul {G : Type u} [group G] {a b c : G} :
a * b⁻¹ = c a = c * b

theorem mul_inv_eq_one {G : Type u} [group G] {a b : G} :
a * b⁻¹ = 1 a = b

theorem add_neg_eq_zero {G : Type u} [add_group G] {a b : G} :
a + -b = 0 a = b

theorem inv_mul_eq_one {G : Type u} [group G] {a b : G} :
a⁻¹ * b = 1 a = b

theorem neg_add_eq_zero {G : Type u} [add_group G] {a b : G} :
-a + b = 0 a = b

@[simp]
theorem add_left_eq_self {G : Type u} [add_group G] {a b : G} :
a + b = b a = 0

@[simp]
theorem mul_left_eq_self {G : Type u} [group G] {a b : G} :
a * b = b a = 1

@[simp]
theorem add_right_eq_self {G : Type u} [add_group G] {a b : G} :
a + b = a b = 0

@[simp]
theorem mul_right_eq_self {G : Type u} [group G] {a b : G} :
a * b = a b = 1

@[simp]
theorem sub_self {G : Type u} [add_group G] (a : G) :
a - a = 0

@[simp]
theorem sub_add_cancel {G : Type u} [add_group G] (a b : G) :
a - b + b = a

@[simp]
theorem add_sub_cancel {G : Type u} [add_group G] (a b : G) :
a + b - b = a

theorem add_sub_assoc {G : Type u} [add_group G] (a b c : G) :
a + b - c = a + (b - c)

theorem eq_of_sub_eq_zero {G : Type u} [add_group G] {a b : G} :
a - b = 0a = b

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

theorem sub_eq_zero_iff_eq {G : Type u} [add_group G] {a b : G} :
a - b = 0 a = b

@[simp]
theorem zero_sub {G : Type u} [add_group G] (a : G) :
0 - a = -a

@[simp]
theorem sub_zero {G : Type u} [add_group G] (a : G) :
a - 0 = a

theorem sub_ne_zero_of_ne {G : Type u} [add_group G] {a b : G} :
a ba - b 0

@[simp]
theorem sub_neg_eq_add {G : Type u} [add_group G] (a b : G) :
a - -b = a + b

@[simp]
theorem neg_sub {G : Type u} [add_group G] (a b : G) :
-(a - b) = b - a

theorem add_sub {G : Type u} [add_group G] (a b c : G) :
a + (b - c) = a + b - c

theorem sub_add_eq_sub_sub_swap {G : Type u} [add_group G] (a b c : G) :
a - (b + c) = a - c - b

@[simp]
theorem add_sub_add_right_eq_sub {G : Type u} [add_group G] (a b c : G) :
a + c - (b + c) = a - b

theorem eq_sub_of_add_eq {G : Type u} [add_group G] {a b c : G} :
a + c = ba = b - c

theorem sub_eq_of_eq_add {G : Type u} [add_group G] {a b c : G} :
a = c + ba - b = c

theorem eq_add_of_sub_eq {G : Type u} [add_group G] {a b c : G} :
a - c = ba = b + c

theorem add_eq_of_eq_sub {G : Type u} [add_group G] {a b c : G} :
a = c - ba + b = c

@[simp]
theorem sub_right_inj {G : Type u} [add_group G] {a b c : G} :
a - b = a - c b = c

@[simp]
theorem sub_left_inj {G : Type u} [add_group G] {a b c : G} :
b - a = c - a b = c

theorem sub_add_sub_cancel {G : Type u} [add_group G] (a b c : G) :
a - b + (b - c) = a - c

theorem sub_sub_sub_cancel_right {G : Type u} [add_group G] (a b c : G) :
a - c - (b - c) = a - b

theorem sub_sub_assoc_swap {G : Type u} [add_group G] {a b c : G} :
a - (b - c) = a + c - b

theorem sub_eq_zero {G : Type u} [add_group G] {a b : G} :
a - b = 0 a = b

theorem sub_ne_zero {G : Type u} [add_group G] {a b : G} :
a - b 0 a b

theorem eq_sub_iff_add_eq {G : Type u} [add_group G] {a b c : G} :
a = b - c a + c = b

theorem sub_eq_iff_eq_add {G : Type u} [add_group G] {a b c : G} :
a - b = c a = c + b

theorem eq_iff_eq_of_sub_eq_sub {G : Type u} [add_group G] {a b c d : G} :
a - b = c - d(a = b c = d)

theorem left_inverse_sub_add_left {G : Type u} [add_group G] (c : G) :
function.left_inverse (λ (x : G), x - c) (λ (x : G), x + c)

theorem left_inverse_add_left_sub {G : Type u} [add_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} [add_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} [add_group G] (c : G) :
function.left_inverse (λ (x : G), -c + x) (λ (x : G), c + x)

theorem mul_inv {G : Type u} [comm_group G] (a b : G) :
(a * b)⁻¹ = a⁻¹ * b⁻¹

theorem neg_add {G : Type u} [add_comm_group G] (a b : G) :
-(a + b) = -a + -b

theorem sub_add_eq_sub_sub {G : Type u} [add_comm_group G] (a b c : G) :
a - (b + c) = a - b - c

theorem neg_add_eq_sub {G : Type u} [add_comm_group G] (a b : G) :
-a + b = b - a

theorem sub_add_eq_add_sub {G : Type u} [add_comm_group G] (a b c : G) :
a - b + c = a + c - b

theorem sub_sub {G : Type u} [add_comm_group G] (a b c : G) :
a - b - c = a - (b + c)

theorem sub_add {G : Type u} [add_comm_group G] (a b c : G) :
a - b + c = a - (b - c)

@[simp]
theorem add_sub_add_left_eq_sub {G : Type u} [add_comm_group G] (a b c : G) :
c + a - (c + b) = a - b

theorem eq_sub_of_add_eq' {G : Type u} [add_comm_group G] {a b c : G} :
c + a = ba = b - c

theorem sub_eq_of_eq_add' {G : Type u} [add_comm_group G] {a b c : G} :
a = b + ca - b = c

theorem eq_add_of_sub_eq' {G : Type u} [add_comm_group G] {a b c : G} :
a - b = ca = b + c

theorem add_eq_of_eq_sub' {G : Type u} [add_comm_group G] {a b c : G} :
b = c - aa + b = c

theorem sub_sub_self {G : Type u} [add_comm_group G] (a b : G) :
a - (a - b) = b

theorem add_sub_comm {G : Type u} [add_comm_group G] (a b c d : G) :
a + b - (c + d) = a - c + (b - d)

theorem sub_eq_sub_add_sub {G : Type u} [add_comm_group G] (a b c : G) :
a - b = c - b + (a - c)

theorem neg_neg_sub_neg {G : Type u} [add_comm_group G] (a b : G) :
-(-a - -b) = a - b

@[simp]
theorem sub_sub_cancel {G : Type u} [add_comm_group G] (a b : G) :
a - (a - b) = b

theorem sub_eq_neg_add {G : Type u} [add_comm_group G] (a b : G) :
a - b = -b + a

theorem neg_add' {G : Type u} [add_comm_group G] (a b : G) :
-(a + b) = -a - b

@[simp]
theorem neg_sub_neg {G : Type u} [add_comm_group G] (a b : G) :
-a - -b = b - a

theorem eq_sub_iff_add_eq' {G : Type u} [add_comm_group G] {a b c : G} :
a = b - c c + a = b

theorem sub_eq_iff_eq_add' {G : Type u} [add_comm_group G] {a b c : G} :
a - b = c a = b + c

@[simp]
theorem add_sub_cancel' {G : Type u} [add_comm_group G] (a b : G) :
a + b - a = b

@[simp]
theorem add_sub_cancel'_right {G : Type u} [add_comm_group G] (a b : G) :
a + (b - a) = b

theorem add_add_neg_cancel'_right {G : Type u} [add_comm_group G] (a b : G) :
a + (b + -a) = b

theorem sub_right_comm {G : Type u} [add_comm_group G] (a b c : G) :
a - b - c = a - c - b

@[simp]
theorem add_add_sub_cancel {G : Type u} [add_comm_group G] (a b c : G) :
a + c + (b - c) = a + b

@[simp]
theorem sub_add_add_cancel {G : Type u} [add_comm_group G] (a b c : G) :
a - c + (b + c) = a + b

@[simp]
theorem sub_add_sub_cancel' {G : Type u} [add_comm_group G] (a b c : G) :
a - b + (c - a) = c - b

@[simp]
theorem add_sub_sub_cancel {G : Type u} [add_comm_group G] (a b c : G) :
a + b - (a - c) = b + c

@[simp]
theorem sub_sub_sub_cancel_left {G : Type u} [add_comm_group G] (a b c : G) :
c - a - (c - b) = b - a

theorem sub_eq_sub_iff_add_eq_add {G : Type u} [add_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} [add_comm_group G] {a b c d : G} :
a - b = c - d a - c = b - d