• 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 (*).

• 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 (+).

• 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 (*).

• 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 (+).

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

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

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

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

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

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

• 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 (*).

• 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 (+).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• 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 (*).

• 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 (+).