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.

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

left_mul g denotes left multiplication by g

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

left_add g denotes left addition by g

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

right_add g denotes right addition by g

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

right_mul g denotes right multiplication by g

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

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

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

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

@[class]
structure comm_semigroup  :
Type uType 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
@[instance]
def comm_semigroup.to_semigroup (G : Type u) [s : comm_semigroup G] :

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

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

@[instance]

@[class]
structure left_cancel_semigroup  :
Type uType 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_1b = c_1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[instance]
def monoid_to_is_left_id {M : Type u} [monoid M] :

@[instance]

@[instance]

@[instance]
def monoid_to_is_right_id {M : Type u} [monoid M] :

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

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

@[instance]

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

@[instance]

@[class]
structure add_comm_monoid  :
Type uType 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
@[class]
structure add_left_cancel_monoid  :
Type uType 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_1b = 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
@[class]
structure left_cancel_monoid  :
Type uType 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_1b = 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
@[instance]

@[class]
structure add_left_cancel_comm_monoid  :
Type uType 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_1b = 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
@[class]
structure left_cancel_comm_monoid  :
Type uType 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_1b = 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
@[class]
structure add_right_cancel_monoid  :
Type uType 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 + ba = 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
@[instance]

@[class]
structure right_cancel_monoid  :
Type uType 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 * ba = 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
@[class]
structure add_right_cancel_comm_monoid  :
Type uType 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 + ba = 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
@[class]
structure right_cancel_comm_monoid  :
Type uType 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 * ba = 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
@[class]
structure add_cancel_monoid  :
Type uType 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_1b = 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 + ba = 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
@[class]
structure cancel_monoid  :
Type uType 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_1b = 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 * ba = c_1

A monoid in which multiplication is cancellative.

Instances
@[class]
structure add_cancel_comm_monoid  :
Type uType 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_1b = 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 + ba = c_1

Commutative version of add_cancel_monoid.

Instances
@[class]
structure cancel_comm_monoid  :
Type uType 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_1b = 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 * ba = c_1

Commutative version of cancel_monoid.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations
@[instance]

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

The subtraction operation on an add_group

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

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

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

@[class]
structure comm_group  :
Type uType 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
@[instance]
def comm_group.to_comm_monoid (G : Type u) [s : comm_group G] :

@[class]
structure add_comm_group  :
Type uType 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
@[instance]

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