algebra.group.basic - mathlib docs

source

theorem comp_assoc_left {α : Type u} (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.

source

theorem comp_assoc_right {α : Type u} (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.

source

@[simp]

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

has_add.add x ∘ has_add.add y = has_add.add (x + y)

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

source

@[simp]

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

has_mul.mul x ∘ has_mul.mul y = has_mul.mul (x * y)

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

source

@[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.

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem one_mul_eq_id {M : Type u} [mul_one_class M] :

has_mul.mul 1 = id

source

theorem zero_add_eq_id {M : Type u} [add_zero_class M] :

has_add.add 0 = id

source

theorem add_zero_eq_id {M : Type u} [add_zero_class M] :

(λ (_x : M), _x + 0) = id

source

theorem mul_one_eq_id {M : Type u} [mul_one_class M] :

(λ (_x : M), _x * 1) = id

source

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

a * b * c = b * a * c

source

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

a + (b + c) = b + (a + c)

source

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

(a * b) * c = (a * c) * b

source

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

a + b + c = a + c + b

source

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)

source

theorem mul_mul_mul_comm {G : Type u} [comm_semigroup G] (a b c d : G) :

(a * b) * c * d = (a * c) * b * d

source

theorem add_rotate {G : Type u} [add_comm_semigroup G] (a b c : G) :

a + b + c = b + c + a

source

theorem mul_rotate {G : Type u} [comm_semigroup G] (a b c : G) :

(a * b) * c = (b * c) * a

source

theorem add_rotate' {G : Type u} [add_comm_semigroup G] (a b c : G) :

a + (b + c) = b + (c + a)

source

theorem mul_rotate' {G : Type u} [comm_semigroup G] (a b c : G) :

a * b * c = b * c * a

source

@[simp]

theorem bit0_zero {M : Type u} [add_monoid M] :

bit0 0 = 0

source

@[simp]

theorem bit1_zero {M : Type u} [add_monoid M] [has_one M] :

bit1 0 = 1

source

theorem inv_unique {M : Type u} [comm_monoid M] {x y z : M} (hy : x * y = 1) (hz : x * z = 1) :

y = z

source

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

y = z

source

@[simp]

theorem add_right_eq_self {M : Type u} [add_left_cancel_monoid M] {a b : M} :

a + b = a ↔ b = 0

source

@[simp]

theorem mul_right_eq_self {M : Type u} [left_cancel_monoid M] {a b : M} :

a * b = a ↔ b = 1

source

@[simp]

theorem self_eq_mul_right {M : Type u} [left_cancel_monoid M] {a b : M} :

a = a * b ↔ b = 1

source

@[simp]

theorem self_eq_add_right {M : Type u} [add_left_cancel_monoid M] {a b : M} :

a = a + b ↔ b = 0

source

@[simp]

theorem add_left_eq_self {M : Type u} [add_right_cancel_monoid M] {a b : M} :

a + b = b ↔ a = 0

source

@[simp]

theorem mul_left_eq_self {M : Type u} [right_cancel_monoid M] {a b : M} :

a * b = b ↔ a = 1

source

@[simp]

theorem self_eq_add_left {M : Type u} [add_right_cancel_monoid M] {a b : M} :

b = a + b ↔ a = 0

source

@[simp]

theorem self_eq_mul_left {M : Type u} [right_cancel_monoid M] {a b : M} :

b = a * b ↔ a = 1

source

@[simp]

theorem inv_involutive {G : Type u} [has_involutive_inv G] :

function.involutive has_inv.inv

source

@[simp]

theorem neg_involutive {G : Type u} [has_involutive_neg G] :

function.involutive has_neg.neg

source

@[simp]

theorem neg_surjective {G : Type u} [has_involutive_neg G] :

function.surjective has_neg.neg

source

@[simp]

theorem inv_surjective {G : Type u} [has_involutive_inv G] :

function.surjective has_inv.inv

source

theorem neg_injective {G : Type u} [has_involutive_neg G] :

function.injective has_neg.neg

source

theorem inv_injective {G : Type u} [has_involutive_inv G] :

function.injective has_inv.inv

source

@[simp]

theorem inv_inj {G : Type u} [has_involutive_inv G] {a b : G} :

a⁻¹ = b⁻¹ ↔ a = b

source

@[simp]

theorem neg_inj {G : Type u} [has_involutive_neg G] {a b : G} :

-a = -b ↔ a = b

source

theorem eq_inv_of_eq_inv {G : Type u} [has_involutive_inv G] {a b : G} (h : a = b⁻¹) :

b = a⁻¹

source

theorem eq_neg_of_eq_neg {G : Type u} [has_involutive_neg G] {a b : G} (h : a = -b) :

b = -a

source

theorem eq_inv_iff_eq_inv {G : Type u} [has_involutive_inv G] {a b : G} :

a = b⁻¹ ↔ b = a⁻¹

source

theorem eq_neg_iff_eq_neg {G : Type u} [has_involutive_neg G] {a b : G} :

a = -b ↔ b = -a

source

theorem neg_eq_iff_neg_eq {G : Type u} [has_involutive_neg G] {a b : G} :

-a = b ↔ -b = a

source

theorem inv_eq_iff_inv_eq {G : Type u} [has_involutive_inv G] {a b : G} :

a⁻¹ = b ↔ b⁻¹ = a

source

theorem neg_eq_zero_sub {G : Type u} [sub_neg_monoid G] (x : G) :

-x = 0 - x

source

theorem inv_eq_one_div {G : Type u} [div_inv_monoid G] (x : G) :

x⁻¹ = 1 / x

source

theorem add_zero_sub {G : Type u} [sub_neg_monoid G] (x y : G) :

x + (0 - y) = x - y

source

theorem mul_one_div {G : Type u} [div_inv_monoid G] (x y : G) :

x * (1 / y) = x / y

source

theorem mul_div_assoc {G : Type u} [div_inv_monoid G] (a b c : G) :

a * b / c = a * (b / c)

source

theorem add_sub_assoc {G : Type u} [sub_neg_monoid G] (a b c : G) :

a + b - c = a + (b - c)

source

theorem add_sub_assoc' {G : Type u} [sub_neg_monoid G] (a b c : G) :

a + (b - c) = a + b - c

source

theorem mul_div_assoc' {G : Type u} [div_inv_monoid G] (a b c : G) :

a * (b / c) = a * b / c

source

@[simp]

theorem one_div {G : Type u} [div_inv_monoid G] (a : G) :

1 / a = a⁻¹

source

@[simp]

theorem zero_sub {G : Type u} [sub_neg_monoid G] (a : G) :

0 - a = -a

source

theorem mul_div {G : Type u} [div_inv_monoid G] (a b c : G) :

a * (b / c) = a * b / c

source

theorem add_sub {G : Type u} [sub_neg_monoid G] (a b c : G) :

a + (b - c) = a + b - c

source

@[simp]

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

a + -b + b = a

source

@[simp]

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

(a * b⁻¹) * b = a

source

@[simp]

theorem one_inv {G : Type u} [group G] :

1⁻¹ = 1

source

@[simp]

theorem neg_zero {G : Type u} [add_group G] :

-0 = 0

source

theorem left_inverse_neg (G : Type u_1) [has_involutive_neg G] :

function.left_inverse (λ (a : G), -a) (λ (a : G), -a)

source

theorem left_inverse_inv (G : Type u_1) [has_involutive_inv G] :

function.left_inverse (λ (a : G), a⁻¹) (λ (a : G), a⁻¹)

source

@[simp]

theorem inv_eq_one {G : Type u} [group G] {a : G} :

a⁻¹ = 1 ↔ a = 1

source

@[simp]

theorem neg_eq_zero {G : Type u} [add_group G] {a : G} :

-a = 0 ↔ a = 0

source

@[simp]

theorem one_eq_inv {G : Type u} [group G] {a : G} :

1 = a⁻¹ ↔ a = 1

source

@[simp]

theorem zero_eq_neg {G : Type u} [add_group G] {a : G} :

0 = -a ↔ a = 0

source

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

a⁻¹ ≠ 1 ↔ a ≠ 1

source

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

-a ≠ 0 ↔ a ≠ 0

source

@[simp]

theorem sub_eq_neg_self {G : Type u} [add_group G] {a b : G} :

a - b = -b ↔ a = 0

source

@[simp]

theorem div_eq_inv_self {G : Type u} [group G] {a b : G} :

a / b = b⁻¹ ↔ a = 1

source

@[simp]

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

a * a⁻¹ * b = b

source

@[simp]

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

a + (-a + b) = b

source

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

function.surjective (has_mul.mul a)

source

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

function.surjective (has_add.add a)

source

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

function.surjective (λ (x : G), x + a)

source

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

function.surjective (λ (x : G), x * a)

source

@[simp]

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

(a * b)⁻¹ = b⁻¹ * a⁻¹

source

@[simp]

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

-(a + b) = -b + -a

source

theorem eq_inv_of_mul_eq_one {G : Type u} [group G] {a b : G} (h : a * b = 1) :

a = b⁻¹

source

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

a = -b

source

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

a = b + -c

source

theorem eq_mul_inv_of_mul_eq {G : Type u} [group G] {a b c : G} (h : a * c = b) :

a = b * c⁻¹

source

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

a = -b + c

source

theorem eq_inv_mul_of_mul_eq {G : Type u} [group G] {a b c : G} (h : b * a = c) :

a = b⁻¹ * c

source

theorem inv_mul_eq_of_eq_mul {G : Type u} [group G] {a b c : G} (h : b = a * c) :

a⁻¹ * b = c

source

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

-a + b = c

source

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

a + -b = c

source

theorem mul_inv_eq_of_eq_mul {G : Type u} [group G] {a b c : G} (h : a = c * b) :

a * b⁻¹ = c

source

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

a = b + c

source

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

a = b * c

source

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

a = b * c

source

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

a = b + c

source

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

a * b = c

source

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

a + b = c

source

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

a * b = c

source

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

a + b = c

source

theorem mul_eq_one_iff_eq_inv {G : Type u} [group G] {a b : G} :

a * b = 1 ↔ a = b⁻¹

source

theorem add_eq_zero_iff_eq_neg {G : Type u} [add_group G] {a b : G} :

a + b = 0 ↔ a = -b

source

theorem mul_eq_one_iff_inv_eq {G : Type u} [group G] {a b : G} :

a * b = 1 ↔ a⁻¹ = b

source

theorem add_eq_zero_iff_neg_eq {G : Type u} [add_group G] {a b : G} :

a + b = 0 ↔ -a = b

source

theorem eq_inv_iff_mul_eq_one {G : Type u} [group G] {a b : G} :

a = b⁻¹ ↔ a * b = 1

source

theorem eq_neg_iff_add_eq_zero {G : Type u} [add_group G] {a b : G} :

a = -b ↔ a + b = 0

source

theorem neg_eq_iff_add_eq_zero {G : Type u} [add_group G] {a b : G} :

-a = b ↔ a + b = 0

source

theorem inv_eq_iff_mul_eq_one {G : Type u} [group G] {a b : G} :

a⁻¹ = b ↔ a * b = 1

source

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

a = b + -c ↔ a + c = b

source

theorem eq_mul_inv_iff_mul_eq {G : Type u} [group G] {a b c : G} :

a = b * c⁻¹ ↔ a * c = b

source

theorem eq_inv_mul_iff_mul_eq {G : Type u} [group G] {a b c : G} :

a = b⁻¹ * c ↔ b * a = c

source

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

a = -b + c ↔ b + a = c

source

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

-a + b = c ↔ b = a + c

source

theorem inv_mul_eq_iff_eq_mul {G : Type u} [group G] {a b c : G} :

a⁻¹ * b = c ↔ b = a * c

source

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

a + -b = c ↔ a = c + b

source

theorem mul_inv_eq_iff_eq_mul {G : Type u} [group G] {a b c : G} :

a * b⁻¹ = c ↔ a = c * b

source

theorem mul_inv_eq_one {G : Type u} [group G] {a b : G} :

a * b⁻¹ = 1 ↔ a = b

source

theorem add_neg_eq_zero {G : Type u} [add_group G] {a b : G} :

a + -b = 0 ↔ a = b

source

theorem inv_mul_eq_one {G : Type u} [group G] {a b : G} :

a⁻¹ * b = 1 ↔ a = b

source

theorem neg_add_eq_zero {G : Type u} [add_group G] {a b : G} :

-a + b = 0 ↔ a = b

source

theorem sub_left_injective {G : Type u} [add_group G] {b : G} :

function.injective (λ (a : G), a - b)

source

theorem div_left_injective {G : Type u} [group G] {b : G} :

function.injective (λ (a : G), a / b)

source

theorem div_right_injective {G : Type u} [group G] {b : G} :

function.injective (λ (a : G), b / a)

source

theorem sub_right_injective {G : Type u} [add_group G] {b : G} :

function.injective (λ (a : G), b - a)

source

@[simp]

theorem inv_div' {G : Type u} [group G] (a b : G) :

(a / b)⁻¹ = b / a

source

@[simp]

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

-(a - b) = b - a

source

@[simp]

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

a - b + b = a

source

@[simp]

theorem div_mul_cancel' {G : Type u} [group G] (a b : G) :

(a / b) * b = a

source

@[simp]

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

a / a = 1

source

@[simp]

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

a - a = 0

source

@[simp]

theorem mul_div_cancel'' {G : Type u} [group G] (a b : G) :

a * b / b = a

source

@[simp]

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

a + b - b = a

source

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

a = b

source

theorem eq_of_div_eq_one' {G : Type u} [group G] {a b : G} (h : a / b = 1) :

a = b

source

theorem div_ne_one_of_ne {G : Type u} [group G] {a b : G} (h : a ≠ b) :

a / b ≠ 1

source

theorem sub_ne_zero_of_ne {G : Type u} [add_group G] {a b : G} (h : a ≠ b) :

a - b ≠ 0

source

@[simp]

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

a - -b = a + b

source

@[simp]

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

a / b⁻¹ = a * b

source

theorem div_mul_eq_div_div_swap {G : Type u} [group G] (a b c : G) :

a / b * c = a / c / b

source

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

a - (b + c) = a - c - b

source

@[simp]

theorem mul_div_mul_right_eq_div {G : Type u} [group G] (a b c : G) :

a * c / b * c = a / b

source

@[simp]

theorem add_sub_add_right_eq_sub {G : Type u} [add_group G] (a b c : G) :

a + c - (b + c) = a - b

source

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

a = b - c

source

theorem eq_div_of_mul_eq' {G : Type u} [group G] {a b c : G} (h : a * c = b) :

a = b / c

source

theorem div_eq_of_eq_mul'' {G : Type u} [group G] {a b c : G} (h : a = c * b) :

a / b = c

source

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

a - b = c

source

theorem eq_mul_of_div_eq {G : Type u} [group G] {a b c : G} (h : a / c = b) :

a = b * c

source

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

a = b + c

source

theorem mul_eq_of_eq_div {G : Type u} [group G] {a b c : G} (h : a = c / b) :

a * b = c

source

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

a + b = c

source

@[simp]

theorem div_right_inj {G : Type u} [group G] {a b c : G} :

a / b = a / c ↔ b = c

source

@[simp]

theorem sub_right_inj {G : Type u} [add_group G] {a b c : G} :

a - b = a - c ↔ b = c

source

@[simp]

theorem div_left_inj {G : Type u} [group G] {a b c : G} :

b / a = c / a ↔ b = c

source

@[simp]

theorem sub_left_inj {G : Type u} [add_group G] {a b c : G} :

b - a = c - a ↔ b = c

source

@[simp]

theorem div_mul_div_cancel' {G : Type u} [group G] (a b c : G) :

(a / b) * (b / c) = a / c

source

@[simp]

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

a - b + (b - c) = a - c

source

@[simp]

theorem div_div_div_cancel_right' {G : Type u} [group G] (a b c : G) :

a / c / (b / c) = a / b

source

@[simp]

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

a - c - (b - c) = a - b

source

theorem sub_sub_assoc_swap {G : Type u} [add_group G] {a b c : G} :

a - (b - c) = a + c - b

source

theorem div_div_assoc_swap {G : Type u} [group G] {a b c : G} :

a / (b / c) = a * c / b

source

theorem div_eq_one {G : Type u} [group G] {a b : G} :

a / b = 1 ↔ a = b

source

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

a - b = 0 ↔ a = b

source

theorem div_eq_one_of_eq {G : Type u} [group G] {a b : G} :

a = b → a / b = 1

Alias of div_eq_one.

source

theorem sub_eq_zero_of_eq {G : Type u} [add_group G] {a b : G} :

a = b → a - b = 0

Alias of sub_eq_zero.

source

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

a - b ≠ 0 ↔ a ≠ b

source

theorem div_ne_one {G : Type u} [group G] {a b : G} :

a / b ≠ 1 ↔ a ≠ b

source

@[simp]

theorem sub_eq_self {G : Type u} [add_group G] {a b : G} :

a - b = a ↔ b = 0

source

@[simp]

theorem div_eq_self {G : Type u} [group G] {a b : G} :

a / b = a ↔ b = 1

source

@[simp]

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

a - 0 = a

source

@[simp]

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

a / 1 = a

source

theorem eq_div_iff_mul_eq' {G : Type u} [group G] {a b c : G} :

a = b / c ↔ a * c = b

source

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

a = b - c ↔ a + c = b

source

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

a - b = c ↔ a = c + b

source

theorem div_eq_iff_eq_mul {G : Type u} [group G] {a b c : G} :

a / b = c ↔ a = c * b

source

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

a = b ↔ c = d

source

theorem eq_iff_eq_of_div_eq_div {G : Type u} [group G] {a b c d : G} (H : a / b = c / d) :

a = b ↔ c = d

source

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)

source

theorem left_inverse_div_mul_left {G : Type u} [group G] (c : G) :

function.left_inverse (λ (x : G), x / c) (λ (x : G), x * c)

source

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)

source

theorem left_inverse_mul_left_div {G : Type u} [group G] (c : G) :

function.left_inverse (λ (x : G), x * c) (λ (x : G), x / c)

source

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)

source

theorem left_inverse_mul_right_inv_mul {G : Type u} [group G] (c : G) :

function.left_inverse (λ (x : G), c * x) (λ (x : G), c⁻¹ * x)

source

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)

source

theorem left_inverse_inv_mul_mul_right {G : Type u} [group G] (c : G) :

function.left_inverse (λ (x : G), c⁻¹ * x) (λ (x : G), c * x)

source

theorem exists_npow_eq_one_of_zpow_eq_one {G : Type u} [group G] {n : ℤ} (hn : n ≠ 0) {x : G} (h : x ^ n = 1) :

∃ (n : ℕ), 0 < n ∧ x ^ n = 1

source

theorem exists_nsmul_eq_zero_of_zsmul_eq_zero {G : Type u} [add_group G] {n : ℤ} (hn : n ≠ 0) {x : G} (h : n • x = 0) :

∃ (n : ℕ), 0 < n ∧ n • x = 0

source

theorem mul_inv {G : Type u} [comm_group G] (a b : G) :

(a * b)⁻¹ = a⁻¹ * b⁻¹

source

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

-(a + b) = -a + -b

source

theorem div_eq_of_eq_mul' {G : Type u} [comm_group G] {a b c : G} (h : a = b * c) :

a / b = c

source

theorem sub_eq_of_eq_add' {G : Type u} [add_comm_group G] {a b c : G} (h : a = b + c) :

a - b = c

source

theorem add_sub_left_comm {G : Type u} [add_comm_group G] {x y z : G} :

x + (y - z) = y + (x - z)

source

theorem mul_div_left_comm {G : Type u} [comm_group G] {x y z : G} :

x * (y / z) = y * (x / z)

source

theorem div_mul_div_comm {G : Type u} [comm_group G] (a b c d : G) :

(a / b) * (c / d) = a * c / b * d

source

theorem sub_add_sub_comm {G : Type u} [add_comm_group G] (a b c d : G) :

a - b + (c - d) = a + c - (b + d)

source

theorem div_div_div_comm {G : Type u} [comm_group G] (a b c d : G) :

a / b / (c / d) = a / c / (b / d)

source

theorem sub_sub_sub_comm {G : Type u} [add_comm_group G] (a b c d : G) :

a - b - (c - d) = a - c - (b - d)

source

theorem div_mul_eq_div_div {G : Type u} [comm_group G] (a b c : G) :

a / b * c = a / b / c

source

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

a - (b + c) = a - b - c

source

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

-a + b = b - a

source

theorem inv_mul_eq_div {G : Type u} [comm_group G] (a b : G) :

a⁻¹ * b = b / a

source

theorem div_mul_eq_mul_div' {G : Type u} [comm_group G] (a b c : G) :

(a / b) * c = a * c / b

source

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

a - b + c = a + c - b

source

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

a - b - c = a - (b + c)

source

theorem div_div {G : Type u} [comm_group G] (a b c : G) :

a / b / c = a / b * c

source

theorem div_mul {G : Type u} [comm_group G] (a b c : G) :

(a / b) * c = a / (b / c)

source

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

a - b + c = a - (b - c)

source

@[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

source

@[simp]

theorem mul_div_mul_left_eq_div {G : Type u} [comm_group G] (a b c : G) :

c * a / c * b = a / b

source

theorem eq_div_of_mul_eq'' {G : Type u} [comm_group G] {a b c : G} (h : c * a = b) :

a = b / c

source

theorem eq_sub_of_add_eq' {G : Type u} [add_comm_group G] {a b c : G} (h : c + a = b) :

a = b - c

source

theorem eq_mul_of_div_eq' {G : Type u} [comm_group G] {a b c : G} (h : a / b = c) :

a = b * c

source

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

a = b + c

source

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

a + b = c

source

theorem mul_eq_of_eq_div' {G : Type u} [comm_group G] {a b c : G} (h : b = c / a) :

a * b = c

source

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

a - (a - b) = b

source

theorem div_div_self' {G : Type u} [comm_group G] (a b : G) :

a / (a / b) = b

source

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

a + b - (c + d) = a - c + (b - d)

source

theorem mul_div_comm' {G : Type u} [comm_group G] (a b c d : G) :

a * b / c * d = (a / c) * (b / d)

source

theorem div_eq_div_mul_div {G : Type u} [comm_group G] (a b c : G) :

a / b = (c / b) * (a / c)

source

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

a - b = c - b + (a - c)

source

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

-(-a - -b) = a - b

source

theorem inv_inv_div_inv {G : Type u} [comm_group G] (a b : G) :

(a⁻¹ / b⁻¹)⁻¹ = a / b

source

@[simp]

theorem sub_sub_cancel {G : Type u} [add_comm_group G] (a b : G) :

a - (a - b) = b

source

@[simp]

theorem div_div_cancel {G : Type u} [comm_group G] (a b : G) :

a / (a / b) = b

source

theorem div_eq_inv_mul' {G : Type u} [comm_group G] (a b : G) :

a / b = b⁻¹ * a

source

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

a - b = -b + a

source

@[simp]

theorem div_div_cancel_left {G : Type u} [comm_group G] (a b : G) :

a / b / a = b⁻¹

source

@[simp]

theorem sub_sub_cancel_left {G : Type u} [add_comm_group G] (a b : G) :

a - b - a = -b

source

theorem inv_mul' {G : Type u} [comm_group G] (a b : G) :

(a * b)⁻¹ = a⁻¹ / b

source

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

-(a + b) = -a - b

source

@[simp]

theorem inv_div_inv {G : Type u} [comm_group G] (a b : G) :

a⁻¹ / b⁻¹ = b / a

source

@[simp]

theorem neg_sub_neg {G : Type u} [add_comm_group G] (a b : G) :

-a - -b = b - a

source

theorem eq_div_iff_mul_eq'' {G : Type u} [comm_group G] {a b c : G} :

a = b / c ↔ c * a = b

source

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

a = b - c ↔ c + a = b

source

theorem div_eq_iff_eq_mul' {G : Type u} [comm_group G] {a b c : G} :

a / b = c ↔ a = b * c

source

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

a - b = c ↔ a = b + c

source

@[simp]

theorem add_sub_cancel' {G : Type u} [add_comm_group G] (a b : G) :

a + b - a = b

source

@[simp]

theorem mul_div_cancel''' {G : Type u} [comm_group G] (a b : G) :

a * b / a = b

source

@[simp]

theorem add_sub_cancel'_right {G : Type u} [add_comm_group G] (a b : G) :

a + (b - a) = b

source

@[simp]

theorem mul_div_cancel'_right {G : Type u} [comm_group G] (a b : G) :

a * (b / a) = b

source

@[simp]

theorem sub_add_cancel' {G : Type u} [add_comm_group G] (a b : G) :

a - (a + b) = -b

source

@[simp]

theorem div_mul_cancel'' {G : Type u} [comm_group G] (a b : G) :

a / a * b = b⁻¹

source

theorem mul_mul_inv_cancel'_right {G : Type u} [comm_group G] (a b : G) :

a * b * a⁻¹ = b

source

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

a + (b + -a) = b

source

theorem div_right_comm' {G : Type u} [comm_group G] (a b c : G) :

a / b / c = a / c / b

source

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

a - b - c = a - c - b

source

@[simp]

theorem add_add_sub_cancel {G : Type u} [add_comm_group G] (a b c : G) :

a + c + (b - c) = a + b

source

@[simp]

theorem mul_mul_div_cancel {G : Type u} [comm_group G] (a b c : G) :

(a * c) * (b / c) = a * b

source

@[simp]

theorem sub_add_add_cancel {G : Type u} [add_comm_group G] (a b c : G) :

a - c + (b + c) = a + b

source

@[simp]

theorem div_mul_mul_cancel {G : Type u} [comm_group G] (a b c : G) :

(a / c) * b * c = a * b

source

@[simp]

theorem div_mul_div_cancel'' {G : Type u} [comm_group G] (a b c : G) :

(a / b) * (c / a) = c / b

source

@[simp]

theorem sub_add_sub_cancel' {G : Type u} [add_comm_group G] (a b c : G) :

a - b + (c - a) = c - b

source

@[simp]

theorem add_sub_sub_cancel {G : Type u} [add_comm_group G] (a b c : G) :

a + b - (a - c) = b + c

source

@[simp]

theorem mul_div_div_cancel {G : Type u} [comm_group G] (a b c : G) :

a * b / (a / c) = b * c

source

@[simp]

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

c - a - (c - b) = b - a

source

@[simp]

theorem div_div_div_cancel_left {G : Type u} [comm_group G] (a b c : G) :

c / a / (c / b) = b / a

source

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

source

theorem div_eq_div_iff_mul_eq_mul {G : Type u} [comm_group G] {a b c d : G} :

a / b = c / d ↔ a * d = c * b

source

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

source

theorem div_eq_div_iff_div_eq_div {G : Type u} [comm_group G] {a b c d : G} :

a / b = c / d ↔ a / c = b / d

source

@[protected, instance]

def commutator_element {G : Type u_1} [group G] :

has_bracket G G

The commutator of two elements g₁ and g₂.

Equations

commutator_element = {bracket := λ (g₁ g₂ : G), ((g₁ * g₂) * g₁⁻¹) * g₂⁻¹}

source

theorem commutator_element_def {G : Type u_1} [group G] (g₁ g₂ : G) :

⁅g₁,g₂⁆ = ((g₁ * g₂) * g₁⁻¹) * g₂⁻¹

mathlib documentation

Basic lemmas about semigroups, monoids, and groups #