mathlib documentation

algebra.group.defs

Typeclasses for (semi)groups and monoid

In this file we define typeclasses for algebraic structures with one binary operation. The classes are named (add_)?(comm_)?(semigroup|monoid|group), where add_ means that the class uses additive notation and comm_ means that the class assumes that the binary operation is commutative.

The file does not contain any lemmas except for

For basic lemmas about these classes see algebra.group.basic.

source
def left_mul {G : Type u} [has_mul G] :
G → G → G

left_mul g denotes left multiplication by g

Equations
source
def left_add {G : Type u} [has_add G] :
G → G → G

left_add g denotes left addition by g

source
def right_add {G : Type u} [has_add G] :
G → G → G

right_add g denotes right addition by g

source
def right_mul {G : Type u} [has_mul G] :
G → G → G

right_mul g denotes right multiplication by g

Equations
source
@[instance]
def semigroup.to_has_mul (G : Type u) [s : semigroup G] :
has_mul G

source
@[class]
structure semigroup  :
Type u → Type u
  • mul : G → G → G
  • mul_assoc : ∀ (a b c_1 : G), (a * b) * c_1 = a * b * c_1

A semigroup is a type with an associative (*).

Instances
source
@[instance]
def add_semigroup.to_has_add (G : Type u) [s : add_semigroup G] :
has_add G

source
@[class]
structure add_semigroup  :
Type u → Type u
  • add : G → G → G
  • add_assoc : ∀ (a b c_1 : G), a + b + c_1 = a + (b + c_1)

An additive semigroup is a type with an associative (+).

Instances
source
theorem add_assoc {G : Type u} [add_semigroup G] (a b c : G) :
a + b + c = a + (b + c)

source
theorem mul_assoc {G : Type u} [semigroup G] (a b c : G) :
(a * b) * c = a * b * c

source
@[instance]
def add_semigroup.to_is_associative {G : Type u} [add_semigroup G] :
is_associative G has_add.add

source
@[instance]
def semigroup.to_is_associative {G : Type u} [semigroup G] :
is_associative G has_mul.mul

source
@[class]
structure comm_semigroup  :
Type u → Type u
  • mul : G → G → G
  • mul_assoc : ∀ (a b c_1 : G), (a * b) * c_1 = a * b * c_1
  • mul_comm : ∀ (a b : G), a * b = b * a

A commutative semigroup is a type with an associative commutative (*).

Instances
source
@[instance]
def comm_semigroup.to_semigroup (G : Type u) [s : comm_semigroup G] :
semigroup G

source
@[instance]
def add_comm_semigroup.to_add_semigroup (G : Type u) [s : add_comm_semigroup G] :
add_semigroup G

source
@[class]
structure add_comm_semigroup  :
Type u → Type u
  • add : G → G → G
  • add_assoc : ∀ (a b c_1 : G), a + b + c_1 = a + (b + c_1)
  • add_comm : ∀ (a b : G), a + b = b + a

A commutative additive semigroup is a type with an associative commutative (+).

Instances
source
theorem add_comm {G : Type u} [add_comm_semigroup G] (a b : G) :
a + b = b + a

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

source
@[instance]
def comm_semigroup.to_is_commutative {G : Type u} [comm_semigroup G] :
is_commutative G has_mul.mul

source
@[instance]
def add_comm_semigroup.to_is_commutative {G : Type u} [add_comm_semigroup G] :
is_commutative G has_add.add

source
@[instance]
def left_cancel_semigroup.to_semigroup (G : Type u) [s : left_cancel_semigroup G] :
semigroup G

source
@[class]
structure left_cancel_semigroup  :
Type u → Type u
  • mul : G → G → G
  • mul_assoc : ∀ (a b c_1 : G), (a * b) * c_1 = a * b * c_1
  • mul_left_cancel : ∀ (a b c_1 : G), a * b = a * c_1 → b = c_1

A left_cancel_semigroup is a semigroup such that a * b = a * c implies b = c.

Instances
source
@[class]
structure add_left_cancel_semigroup  :
Type u → Type u
  • add : G → G → G
  • add_assoc : ∀ (a b c_1 : G), a + b + c_1 = a + (b + c_1)
  • add_left_cancel : ∀ (a b c_1 : G), a + b = a + c_1 → b = c_1

An add_left_cancel_semigroup is an additive semigroup such that a + b = a + c implies b = c.

Instances
source
@[instance]
def add_left_cancel_semigroup.to_add_semigroup (G : Type u) [s : add_left_cancel_semigroup G] :
add_semigroup G

source
theorem mul_left_cancel {G : Type u} [left_cancel_semigroup G] {a b c : G} :
a * b = a * c → b = c

source
theorem add_left_cancel {G : Type u} [add_left_cancel_semigroup G] {a b c : G} :
a + b = a + c → b = c

source
theorem add_left_cancel_iff {G : Type u} [add_left_cancel_semigroup G] {a b c : G} :
a + b = a + c ↔ b = c

source
theorem mul_left_cancel_iff {G : Type u} [left_cancel_semigroup G] {a b c : G} :
a * b = a * c ↔ b = c

source
theorem add_right_injective {G : Type u} [add_left_cancel_semigroup G] (a : G) :
function.injective (has_add.add a)

source
theorem mul_right_injective {G : Type u} [left_cancel_semigroup G] (a : G) :
function.injective (has_mul.mul a)

source
@[simp]
theorem mul_right_inj {G : Type u} [left_cancel_semigroup G] (a : G) {b c : G} :
a * b = a * c ↔ b = c

source
@[simp]
theorem add_right_inj {G : Type u} [add_left_cancel_semigroup G] (a : G) {b c : G} :
a + b = a + c ↔ b = c

source
@[class]
structure right_cancel_semigroup  :
Type u → Type u
  • mul : G → G → G
  • mul_assoc : ∀ (a b c_1 : G), (a * b) * c_1 = a * b * c_1
  • mul_right_cancel : ∀ (a b c_1 : G), a * b = c_1 * b → a = c_1

A right_cancel_semigroup is a semigroup such that a * b = c * b implies a = c.

Instances
source
@[instance]
def right_cancel_semigroup.to_semigroup (G : Type u) [s : right_cancel_semigroup G] :
semigroup G

source
@[class]
structure add_right_cancel_semigroup  :
Type u → Type u
  • add : G → G → G
  • add_assoc : ∀ (a b c_1 : G), a + b + c_1 = a + (b + c_1)
  • add_right_cancel : ∀ (a b c_1 : G), a + b = c_1 + b → a = c_1

An add_right_cancel_semigroup is an additive semigroup such that a + b = c + b implies a = c.

Instances
source
@[instance]
def add_right_cancel_semigroup.to_add_semigroup (G : Type u) [s : add_right_cancel_semigroup G] :
add_semigroup G

source
theorem mul_right_cancel {G : Type u} [right_cancel_semigroup G] {a b c : G} :
a * b = c * b → a = c

source
theorem add_right_cancel {G : Type u} [add_right_cancel_semigroup G] {a b c : G} :
a + b = c + b → a = c

source
theorem mul_right_cancel_iff {G : Type u} [right_cancel_semigroup G] {a b c : G} :
b * a = c * a ↔ b = c

source
theorem add_right_cancel_iff {G : Type u} [add_right_cancel_semigroup G] {a b c : G} :
b + a = c + a ↔ b = c

source
theorem add_left_injective {G : Type u} [add_right_cancel_semigroup G] (a : G) :
function.injective (λ (x : G), x + a)

source
theorem mul_left_injective {G : Type u} [right_cancel_semigroup G] (a : G) :
function.injective (λ (x : G), x * a)

source
@[simp]
theorem add_left_inj {G : Type u} [add_right_cancel_semigroup G] (a : G) {b c : G} :
b + a = c + a ↔ b = c

source
@[simp]
theorem mul_left_inj {G : Type u} [right_cancel_semigroup G] (a : G) {b c : G} :
b * a = c * a ↔ b = c

source
@[instance]
def monoid.to_has_one (M : Type u) [s : monoid M] :
has_one M

source
@[instance]
def monoid.to_semigroup (M : Type u) [s : monoid M] :
semigroup M

source
@[class]
structure monoid  :
Type u → Type u
  • mul : M → M → M
  • mul_assoc : ∀ (a b c_1 : M), (a * b) * c_1 = a * b * c_1
  • one : M
  • one_mul : ∀ (a : M), 1 * a = a
  • mul_one : ∀ (a : M), a * 1 = a

A monoid is a semigroup with an element 1 such that 1 * a = a * 1 = a.

Instances
source
@[instance]
def add_monoid.to_add_semigroup (M : Type u) [s : add_monoid M] :
add_semigroup M

source
@[instance]
def add_monoid.to_has_zero (M : Type u) [s : add_monoid M] :
has_zero M

source
@[class]
structure add_monoid  :
Type u → Type u
  • add : M → M → M
  • add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
  • zero : M
  • zero_add : ∀ (a : M), 0 + a = a
  • add_zero : ∀ (a : M), a + 0 = a

An add_monoid is an add_semigroup with an element 0 such that 0 + a = a + 0 = a.

Instances
source
@[simp]
theorem one_mul {M : Type u} [monoid M] (a : M) :
1 * a = a

source
@[simp]
theorem zero_add {M : Type u} [add_monoid M] (a : M) :
0 + a = a

source
@[simp]
theorem add_zero {M : Type u} [add_monoid M] (a : M) :
a + 0 = a

source
@[simp]
theorem mul_one {M : Type u} [monoid M] (a : M) :
a * 1 = a

source
@[instance]
def monoid_to_is_left_id {M : Type u} [monoid M] :
is_left_id M has_mul.mul 1

source
@[instance]
def add_monoid_to_is_left_id {M : Type u} [add_monoid M] :
is_left_id M has_add.add 0

source
@[instance]
def add_monoid_to_is_right_id {M : Type u} [add_monoid M] :
is_right_id M has_add.add 0

source
@[instance]
def monoid_to_is_right_id {M : Type u} [monoid M] :
is_right_id M has_mul.mul 1

source
theorem left_inv_eq_right_inv {M : Type u} [monoid M] {a b c : M} :
b * a = 1 → a * c = 1 → b = c

source
theorem left_neg_eq_right_neg {M : Type u} [add_monoid M] {a b c : M} :
b + a = 0 → a + c = 0 → b = c

source
@[instance]
def comm_monoid.to_comm_semigroup (M : Type u) [s : comm_monoid M] :
comm_semigroup M

source
@[class]
structure comm_monoid  :
Type u → Type u
  • mul : M → M → M
  • mul_assoc : ∀ (a b c_1 : M), (a * b) * c_1 = a * b * c_1
  • one : M
  • one_mul : ∀ (a : M), 1 * a = a
  • mul_one : ∀ (a : M), a * 1 = a
  • mul_comm : ∀ (a b : M), a * b = b * a

A commutative monoid is a monoid with commutative (*).

Instances
source
@[instance]
def comm_monoid.to_monoid (M : Type u) [s : comm_monoid M] :
monoid M

source
@[instance]
def add_comm_monoid.to_add_monoid (M : Type u) [s : add_comm_monoid M] :
add_monoid M

source
@[class]
structure add_comm_monoid  :
Type u → Type u
  • add : M → M → M
  • add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
  • zero : M
  • zero_add : ∀ (a : M), 0 + a = a
  • add_zero : ∀ (a : M), a + 0 = a
  • add_comm : ∀ (a b : M), a + b = b + a

An additive commutative monoid is an additive monoid with commutative (+).

Instances
source
@[instance]
def add_comm_monoid.to_add_comm_semigroup (M : Type u) [s : add_comm_monoid M] :
add_comm_semigroup M

source
@[instance]
def add_left_cancel_monoid.to_add_monoid (M : Type u) [s : add_left_cancel_monoid M] :
add_monoid M

source
@[class]
structure add_left_cancel_monoid  :
Type u → Type u
  • add : M → M → M
  • add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
  • add_left_cancel : ∀ (a b c_1 : M), a + b = a + c_1 → b = c_1
  • zero : M
  • zero_add : ∀ (a : M), 0 + a = a
  • add_zero : ∀ (a : M), a + 0 = a

An additive monoid in which addition is left-cancellative. Main examples are ℕ and groups. This is the right typeclass for many sum lemmas, as having a zero is useful to define the sum over the empty set, so add_left_cancel_semigroup is not enough.

Instances
source
@[instance]
def add_left_cancel_monoid.to_add_left_cancel_semigroup (M : Type u) [s : add_left_cancel_monoid M] :
add_left_cancel_semigroup M

source
@[class]
structure left_cancel_monoid  :
Type u → Type u
  • mul : M → M → M
  • mul_assoc : ∀ (a b c_1 : M), (a * b) * c_1 = a * b * c_1
  • mul_left_cancel : ∀ (a b c_1 : M), a * b = a * c_1 → b = c_1
  • one : M
  • one_mul : ∀ (a : M), 1 * a = a
  • mul_one : ∀ (a : M), a * 1 = a

A monoid in which multiplication is left-cancellative.

Instances
source
@[instance]
def left_cancel_monoid.to_left_cancel_semigroup (M : Type u) [s : left_cancel_monoid M] :
left_cancel_semigroup M

source
@[instance]
def left_cancel_monoid.to_monoid (M : Type u) [s : left_cancel_monoid M] :
monoid M

source
@[instance]
def add_left_cancel_comm_monoid.to_add_left_cancel_monoid (M : Type u) [s : add_left_cancel_comm_monoid M] :
add_left_cancel_monoid M

source
@[instance]
def add_left_cancel_comm_monoid.to_add_comm_monoid (M : Type u) [s : add_left_cancel_comm_monoid M] :
add_comm_monoid M

source
@[class]
structure add_left_cancel_comm_monoid  :
Type u → Type u
  • add : M → M → M
  • add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
  • add_left_cancel : ∀ (a b c_1 : M), a + b = a + c_1 → b = c_1
  • zero : M
  • zero_add : ∀ (a : M), 0 + a = a
  • add_zero : ∀ (a : M), a + 0 = a
  • add_comm : ∀ (a b : M), a + b = b + a

Commutative version of add_left_cancel_monoid.

Instances
source
@[instance]
def left_cancel_comm_monoid.to_left_cancel_monoid (M : Type u) [s : left_cancel_comm_monoid M] :
left_cancel_monoid M

source
@[class]
structure left_cancel_comm_monoid  :
Type u → Type u
  • mul : M → M → M
  • mul_assoc : ∀ (a b c_1 : M), (a * b) * c_1 = a * b * c_1
  • mul_left_cancel : ∀ (a b c_1 : M), a * b = a * c_1 → b = c_1
  • one : M
  • one_mul : ∀ (a : M), 1 * a = a
  • mul_one : ∀ (a : M), a * 1 = a
  • mul_comm : ∀ (a b : M), a * b = b * a

Commutative version of left_cancel_monoid.

Instances
source
@[instance]
def left_cancel_comm_monoid.to_comm_monoid (M : Type u) [s : left_cancel_comm_monoid M] :
comm_monoid M

source
@[instance]
def add_right_cancel_monoid.to_add_right_cancel_semigroup (M : Type u) [s : add_right_cancel_monoid M] :
add_right_cancel_semigroup M

source
@[class]
structure add_right_cancel_monoid  :
Type u → Type u
  • add : M → M → M
  • add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
  • add_right_cancel : ∀ (a b c_1 : M), a + b = c_1 + b → a = c_1
  • zero : M
  • zero_add : ∀ (a : M), 0 + a = a
  • add_zero : ∀ (a : M), a + 0 = a

An additive monoid in which addition is right-cancellative. Main examples are ℕ and groups. This is the right typeclass for many sum lemmas, as having a zero is useful to define the sum over the empty set, so add_right_cancel_semigroup is not enough.

Instances
source
@[instance]
def add_right_cancel_monoid.to_add_monoid (M : Type u) [s : add_right_cancel_monoid M] :
add_monoid M

source
@[instance]
def right_cancel_monoid.to_monoid (M : Type u) [s : right_cancel_monoid M] :
monoid M

source
@[class]
structure right_cancel_monoid  :
Type u → Type u
  • mul : M → M → M
  • mul_assoc : ∀ (a b c_1 : M), (a * b) * c_1 = a * b * c_1
  • mul_right_cancel : ∀ (a b c_1 : M), a * b = c_1 * b → a = c_1
  • one : M
  • one_mul : ∀ (a : M), 1 * a = a
  • mul_one : ∀ (a : M), a * 1 = a

A monoid in which multiplication is right-cancellative.

Instances
source
@[instance]
def right_cancel_monoid.to_right_cancel_semigroup (M : Type u) [s : right_cancel_monoid M] :
right_cancel_semigroup M

source
@[class]
structure add_right_cancel_comm_monoid  :
Type u → Type u
  • add : M → M → M
  • add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
  • add_right_cancel : ∀ (a b c_1 : M), a + b = c_1 + b → a = c_1
  • zero : M
  • zero_add : ∀ (a : M), 0 + a = a
  • add_zero : ∀ (a : M), a + 0 = a
  • add_comm : ∀ (a b : M), a + b = b + a

Commutative version of add_right_cancel_monoid.

Instances
source
@[instance]
def add_right_cancel_comm_monoid.to_add_comm_monoid (M : Type u) [s : add_right_cancel_comm_monoid M] :
add_comm_monoid M

source
@[instance]
def add_right_cancel_comm_monoid.to_add_right_cancel_monoid (M : Type u) [s : add_right_cancel_comm_monoid M] :
add_right_cancel_monoid M

source
@[instance]
def right_cancel_comm_monoid.to_right_cancel_monoid (M : Type u) [s : right_cancel_comm_monoid M] :
right_cancel_monoid M

source
@[instance]
def right_cancel_comm_monoid.to_comm_monoid (M : Type u) [s : right_cancel_comm_monoid M] :
comm_monoid M

source
@[class]
structure right_cancel_comm_monoid  :
Type u → Type u
  • mul : M → M → M
  • mul_assoc : ∀ (a b c_1 : M), (a * b) * c_1 = a * b * c_1
  • mul_right_cancel : ∀ (a b c_1 : M), a * b = c_1 * b → a = c_1
  • one : M
  • one_mul : ∀ (a : M), 1 * a = a
  • mul_one : ∀ (a : M), a * 1 = a
  • mul_comm : ∀ (a b : M), a * b = b * a

Commutative version of right_cancel_monoid.

Instances
source
@[instance]
def add_cancel_monoid.to_add_right_cancel_monoid (M : Type u) [s : add_cancel_monoid M] :
add_right_cancel_monoid M

source
@[class]
structure add_cancel_monoid  :
Type u → Type u
  • add : M → M → M
  • add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
  • add_left_cancel : ∀ (a b c_1 : M), a + b = a + c_1 → b = c_1
  • zero : M
  • zero_add : ∀ (a : M), 0 + a = a
  • add_zero : ∀ (a : M), a + 0 = a
  • add_right_cancel : ∀ (a b c_1 : M), a + b = c_1 + b → a = c_1

An additive monoid in which addition is cancellative on both sides. Main examples are ℕ and groups. This is the right typeclass for many sum lemmas, as having a zero is useful to define the sum over the empty set, so add_right_cancel_semigroup is not enough.

Instances
source
@[instance]
def add_cancel_monoid.to_add_left_cancel_monoid (M : Type u) [s : add_cancel_monoid M] :
add_left_cancel_monoid M

source
@[instance]
def cancel_monoid.to_right_cancel_monoid (M : Type u) [s : cancel_monoid M] :
right_cancel_monoid M

source
@[class]
structure cancel_monoid  :
Type u → Type u
  • mul : M → M → M
  • mul_assoc : ∀ (a b c_1 : M), (a * b) * c_1 = a * b * c_1
  • mul_left_cancel : ∀ (a b c_1 : M), a * b = a * c_1 → b = c_1
  • one : M
  • one_mul : ∀ (a : M), 1 * a = a
  • mul_one : ∀ (a : M), a * 1 = a
  • mul_right_cancel : ∀ (a b c_1 : M), a * b = c_1 * b → a = c_1

A monoid in which multiplication is cancellative.

Instances
source
@[instance]
def cancel_monoid.to_left_cancel_monoid (M : Type u) [s : cancel_monoid M] :
left_cancel_monoid M

source
@[instance]
def add_cancel_comm_monoid.to_add_left_cancel_comm_monoid (M : Type u) [s : add_cancel_comm_monoid M] :
add_left_cancel_comm_monoid M

source
@[class]
structure add_cancel_comm_monoid  :
Type u → Type u
  • add : M → M → M
  • add_assoc : ∀ (a b c_1 : M), a + b + c_1 = a + (b + c_1)
  • add_left_cancel : ∀ (a b c_1 : M), a + b = a + c_1 → b = c_1
  • zero : M
  • zero_add : ∀ (a : M), 0 + a = a
  • add_zero : ∀ (a : M), a + 0 = a
  • add_comm : ∀ (a b : M), a + b = b + a
  • add_right_cancel : ∀ (a b c_1 : M), a + b = c_1 + b → a = c_1

Commutative version of add_cancel_monoid.

Instances
source
@[instance]
def add_cancel_comm_monoid.to_add_right_cancel_comm_monoid (M : Type u) [s : add_cancel_comm_monoid M] :
add_right_cancel_comm_monoid M

source
@[class]
structure cancel_comm_monoid  :
Type u → Type u
  • mul : M → M → M
  • mul_assoc : ∀ (a b c_1 : M), (a * b) * c_1 = a * b * c_1
  • mul_left_cancel : ∀ (a b c_1 : M), a * b = a * c_1 → b = c_1
  • one : M
  • one_mul : ∀ (a : M), 1 * a = a
  • mul_one : ∀ (a : M), a * 1 = a
  • mul_comm : ∀ (a b : M), a * b = b * a
  • mul_right_cancel : ∀ (a b c_1 : M), a * b = c_1 * b → a = c_1

Commutative version of cancel_monoid.

Instances
source
@[instance]
def cancel_comm_monoid.to_right_cancel_comm_monoid (M : Type u) [s : cancel_comm_monoid M] :
right_cancel_comm_monoid M

source
@[instance]
def cancel_comm_monoid.to_left_cancel_comm_monoid (M : Type u) [s : cancel_comm_monoid M] :
left_cancel_comm_monoid M

source
@[instance]
def group.to_has_inv (α : Type u) [s : group α] :
has_inv α

source
@[class]
structure group  :
Type u → Type u
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • inv : α → α
  • mul_left_inv : ∀ (a : α), a⁻¹ * a = 1

A group is a monoid with an operation ⁻¹ satisfying a⁻¹ * a = 1.

Instances
source
@[instance]
def group.to_monoid (α : Type u) [s : group α] :
monoid α

source
@[instance]
def add_group.to_has_neg (α : Type u) [s : add_group α] :
has_neg α

source
@[class]
structure add_group  :
Type u → Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • add_left_neg : ∀ (a : α), -a + a = 0

An add_group is an add_monoid with a unary - satisfying -a + a = 0.

Instances
source
@[instance]
def add_group.to_add_monoid (α : Type u) [s : add_group α] :
add_monoid α

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

source
@[simp]
theorem mul_left_inv {G : Type u} [group G] (a : G) :
a⁻¹ * a = 1

source
theorem neg_add_self {G : Type u} [add_group G] (a : G) :
-a + a = 0

source
theorem inv_mul_self {G : Type u} [group G] (a : G) :
a⁻¹ * a = 1

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

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

source
@[simp]
theorem inv_eq_of_mul_eq_one {G : Type u} [group G] {a b : G} :
a * b = 1 → a⁻¹ = b

source
@[simp]
theorem neg_eq_of_add_eq_zero {G : Type u} [add_group G] {a b : G} :
a + b = 0 → -a = b

source
@[simp]
theorem inv_inv {G : Type u} [group G] (a : G) :
a⁻¹⁻¹ = a

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

source
@[simp]
theorem mul_right_inv {G : Type u} [group G] (a : G) :
a * a⁻¹ = 1

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

source
theorem add_neg_self {G : Type u} [add_group G] (a : G) :
a + -a = 0

source
theorem mul_inv_self {G : Type u} [group G] (a : G) :
a * a⁻¹ = 1

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

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

source
@[instance]
def group.to_left_cancel_semigroup {G : Type u} [group G] :
left_cancel_semigroup G

Equations
source
@[instance]
def add_group.to_left_cancel_add_semigroup {G : Type u} [add_group G] :
add_left_cancel_semigroup G

source
@[instance]
def group.to_right_cancel_semigroup {G : Type u} [group G] :
right_cancel_semigroup G

Equations
source
@[instance]
def add_group.to_right_cancel_add_semigroup {G : Type u} [add_group G] :
add_right_cancel_semigroup G

source
@[instance]
def group.to_cancel_monoid {G : Type u} [group G] :
cancel_monoid G

Equations
source
@[instance]
def add_group.to_cancel_add_monoid {G : Type u} [add_group G] :
add_cancel_monoid G

source
def algebra.sub {G : Type u} [add_group G] :
G → G → G

The subtraction operation on an add_group

Equations
source
@[instance]
def add_group_has_sub {G : Type u} [add_group G] :
has_sub G

Equations
source
theorem sub_eq_add_neg {G : Type u} [add_group G] (a b : G) :
a - b = a + -b

source
@[instance]
def comm_group.to_group (G : Type u) [s : comm_group G] :
group G

source
@[class]
structure comm_group  :
Type u → Type u
  • mul : G → G → G
  • mul_assoc : ∀ (a b c_1 : G), (a * b) * c_1 = a * b * c_1
  • one : G
  • one_mul : ∀ (a : G), 1 * a = a
  • mul_one : ∀ (a : G), a * 1 = a
  • inv : G → G
  • mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
  • mul_comm : ∀ (a b : G), a * b = b * a

A commutative group is a group with commutative (*).

Instances
source
@[instance]
def comm_group.to_comm_monoid (G : Type u) [s : comm_group G] :
comm_monoid G

source
@[class]
structure add_comm_group  :
Type u → Type u
  • add : G → G → G
  • add_assoc : ∀ (a b c_1 : G), a + b + c_1 = a + (b + c_1)
  • zero : G
  • zero_add : ∀ (a : G), 0 + a = a
  • add_zero : ∀ (a : G), a + 0 = a
  • neg : G → G
  • add_left_neg : ∀ (a : G), -a + a = 0
  • add_comm : ∀ (a b : G), a + b = b + a

An additive commutative group is an additive group with commutative (+).

Instances
source
@[instance]
def add_comm_group.to_add_comm_monoid (G : Type u) [s : add_comm_group G] :
add_comm_monoid G

source
@[instance]
def add_comm_group.to_add_group (G : Type u) [s : add_comm_group G] :
add_group G

source
@[instance]
def comm_group.to_cancel_comm_monoid {G : Type u} [comm_group G] :
cancel_comm_monoid G

Equations
source
@[instance]
def add_comm_group.to_cancel_add_comm_monoid {G : Type u} [add_comm_group G] :
add_cancel_comm_monoid G