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

axioms of typeclasses restated in the root namespace;
lemmas required for instances.

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

left_mul = λ (g x : G), g * x

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

right_mul = λ (g x : G), x * g

@[instance]

def semigroup.to_has_mul (G : Type u) [self : semigroup G] :

@[class]

structure semigroup (G : 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

@[instance]

def add_semigroup.to_has_add (G : Type u) [self : add_semigroup G] :

@[class]

structure add_semigroup (G : 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

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

@[instance]

def add_semigroup.to_is_associative {G : Type u} [add_semigroup G] :

is_associative G has_add.add

@[instance]

def semigroup.to_is_associative {G : Type u} [semigroup G] :

is_associative G has_mul.mul

@[class]

structure comm_semigroup (G : 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

@[instance]

def comm_semigroup.to_semigroup (G : Type u) [self : comm_semigroup G] :

@[instance]

def add_comm_semigroup.to_add_semigroup (G : Type u) [self : add_comm_semigroup G] :

add_semigroup G

@[class]

structure add_comm_semigroup (G : 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

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]

def comm_semigroup.to_is_commutative {G : Type u} [comm_semigroup G] :

is_commutative G has_mul.mul

@[instance]

def add_comm_semigroup.to_is_commutative {G : Type u} [add_comm_semigroup G] :

is_commutative G has_add.add

@[instance]

def left_cancel_semigroup.to_semigroup (G : Type u) [self : left_cancel_semigroup G] :

@[class]

structure left_cancel_semigroup (G : 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

@[class]

structure add_left_cancel_semigroup (G : 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

@[instance]

def add_left_cancel_semigroup.to_add_semigroup (G : Type u) [self : add_left_cancel_semigroup G] :

add_semigroup G

theorem mul_left_cancel {G : Type u} [left_cancel_semigroup G] {a b c : G} :

a * b = a * c → b = c

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

a + b = a + c → b = 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

theorem add_right_injective {G : Type u} [add_left_cancel_semigroup G] (a : G) :

function.injective (has_add.add a)

theorem mul_right_injective {G : Type u} [left_cancel_semigroup G] (a : G) :

function.injective (has_mul.mul a)

@[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_ne_mul_right {G : Type u} [left_cancel_semigroup G] (a : G) {b c : G} :

a * b ≠ a * c ↔ b ≠ c

theorem add_ne_add_right {G : Type u} [add_left_cancel_semigroup G] (a : G) {b c : G} :

a + b ≠ a + c ↔ b ≠ c

@[class]

structure right_cancel_semigroup (G : 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

@[instance]

def right_cancel_semigroup.to_semigroup (G : Type u) [self : right_cancel_semigroup G] :

@[class]

structure add_right_cancel_semigroup (G : 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

@[instance]

def add_right_cancel_semigroup.to_add_semigroup (G : Type u) [self : add_right_cancel_semigroup G] :

add_semigroup G

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

a * b = c * b → a = c

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

a + b = c + b → a = 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

theorem mul_ne_mul_left {G : Type u} [right_cancel_semigroup G] (a : G) {b c : G} :

b * a ≠ c * a ↔ b ≠ c

theorem add_ne_add_left {G : Type u} [add_right_cancel_semigroup G] (a : G) {b c : G} :

b + a ≠ c + a ↔ b ≠ c

@[class]

structure mul_one_class (M : Type u) :

Type u

one : M
mul : M → M → M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a

Typeclass for expressing that a type M with multiplication and a one satisfies 1 * a = a and a * 1 = a for all a : M.

Instances

@[instance]

def mul_one_class.to_has_one (M : Type u) [self : mul_one_class M] :

@[instance]

def mul_one_class.to_has_mul (M : Type u) [self : mul_one_class M] :

@[instance]

def add_zero_class.to_has_add (M : Type u) [self : add_zero_class M] :

@[instance]

def add_zero_class.to_has_zero (M : Type u) [self : add_zero_class M] :

@[class]

structure add_zero_class (M : Type u) :

Type u

zero : M
add : M → M → M
zero_add : ∀ (a : M), 0 + a = a
add_zero : ∀ (a : M), a + 0 = a

Typeclass for expressing that a type M with addition and a zero satisfies 0 + a = a and a + 0 = a for all a : M.

Instances

@[simp]

theorem one_mul {M : Type u} [mul_one_class M] (a : M) :

1 * a = a

@[simp]

theorem zero_add {M : Type u} [add_zero_class M] (a : M) :

0 + a = a

@[simp]

theorem add_zero {M : Type u} [add_zero_class M] (a : M) :

a + 0 = a

@[simp]

theorem mul_one {M : Type u} [mul_one_class M] (a : M) :

a * 1 = a

@[instance]

def mul_one_class.to_is_left_id {M : Type u} [mul_one_class M] :

is_left_id M has_mul.mul 1

@[instance]

def add_zero_class.to_is_left_id {M : Type u} [add_zero_class M] :

is_left_id M has_add.add 0

@[instance]

def mul_one_class.to_is_right_id {M : Type u} [mul_one_class M] :

is_right_id M has_mul.mul 1

@[instance]

def add_zero_class.to_is_right_id {M : Type u} [add_zero_class M] :

is_right_id M has_add.add 0

def npow_rec {M : Type u} [has_one M] [has_mul M] :

ℕ → M → M

The fundamental power operation in a monoid. npow_rec n a = a*a*...*a n times. Use instead a ^ n, which has better definitional behavior.

Equations

npow_rec (n + 1) a = a * npow_rec n a
npow_rec 0 a = 1

def nsmul_rec {M : Type u} [has_zero M] [has_add M] :

ℕ → M → M

The fundamental scalar multiplication in an additive monoid. nsmul_rec n a = a+a+...+a n times. Use instead n • a, which has better definitional behavior.

Equations

nsmul_rec (n + 1) a = a + nsmul_rec n a
nsmul_rec 0 a = 0

meta def try_refl_tac :

try_refl_tac solves goals of the form ∀ a b, f a b = g a b, if they hold by definition.

Design note on `add_monoid` and `monoid` #

An add_monoid has a natural ℕ-action, defined by n • a = a + ... + a, that we want to declare as an instance as it makes it possible to use the language of linear algebra. However, there are often other natural ℕ-actions. For instance, for any semiring R, the space of polynomials polynomial R has a natural R-action defined by multiplication on the coefficients. This means that polynomial ℕ would have two natural ℕ-actions, which are equal but not defeq. The same goes for linear maps, tensor products, and so on (and even for ℕ itself).

To solve this issue, we embed an ℕ-action in the definition of an add_monoid (which is by default equal to the naive action a + ... + a, but can be adjusted when needed), and declare a has_scalar ℕ α instance using this action. See Note [forgetful inheritance] for more explanations on this pattern.

For example, when we define polynomial R, then we declare the ℕ-action to be by multiplication on each coefficient (using the ℕ-action on R that comes from the fact that R is an add_monoid). In this way, the two natural has_scalar ℕ (polynomial ℕ) instances are defeq.

The tactic to_additive transfers definitions and results from multiplicative monoids to additive monoids. To work, it has to map fields to fields. This means that we should also add corresponding fields to the multiplicative structure monoid, which could solve defeq problems for powers if needed. These problems do not come up in practice, so most of the time we will not need to adjust the npow field when defining multiplicative objects.

Nice notation and a basic theory for the power function on monoids and the ℕ-action on additive monoids are built in the file algebra.group_power.basic. For now, we only register the most basic properties that we need right away.

In the definition, we use n.succ instead of n + 1 in the nsmul_succ' and npow_succ' fields to make sure that to_additive is not confused (otherwise, it would try to convert 1 : ℕ to 0 : ℕ).

@[instance]

def add_monoid.to_add_semigroup (M : Type u) [self : add_monoid M] :

add_semigroup M

@[instance]

def add_monoid.to_add_zero_class (M : Type u) [self : add_monoid M] :

add_zero_class M

@[class]

structure add_monoid (M : 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
nsmul : ℕ → M → M
nsmul_zero' : (∀ (x : M), nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : M), nsmul n.succ x = x + nsmul n x) . "try_refl_tac"

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

Instances

@[instance]

def monoid.to_mul_one_class (M : Type u) [self : monoid M] :

mul_one_class M

@[instance]

def monoid.to_semigroup (M : Type u) [self : monoid M] :

@[class]

structure monoid (M : 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
npow : ℕ → M → M
npow_zero' : (∀ (x : M), npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M), npow n.succ x = x * npow n x) . "try_refl_tac"

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

Instances

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

b = c

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

b = c

theorem npow_one {M : Type u} [monoid M] (x : M) :

npow 1 x = x

theorem nsmul_one' {M : Type u} [add_monoid M] (x : M) :

nsmul 1 x = x

theorem nsmul_add' {M : Type u} [add_monoid M] (m n : ℕ) (x : M) :

nsmul (m + n) x = nsmul m x + nsmul n x

theorem npow_add {M : Type u} [monoid M] (m n : ℕ) (x : M) :

npow (m + n) x = (npow m x) * npow n x

@[instance]

def add_comm_monoid.to_add_monoid (M : Type u) [self : add_comm_monoid M] :

@[class]

structure add_comm_monoid (M : 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
nsmul : ℕ → M → M
nsmul_zero' : (∀ (x : M), add_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : M), add_comm_monoid.nsmul n.succ x = x + add_comm_monoid.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : M), a + b = b + a

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

Instances

@[instance]

def add_comm_monoid.to_add_comm_semigroup (M : Type u) [self : add_comm_monoid M] :

add_comm_semigroup M

@[instance]

def comm_monoid.to_comm_semigroup (M : Type u) [self : comm_monoid M] :

comm_semigroup M

@[class]

structure comm_monoid (M : 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
npow : ℕ → M → M
npow_zero' : (∀ (x : M), comm_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M), comm_monoid.npow n.succ x = x * comm_monoid.npow n x) . "try_refl_tac"
mul_comm : ∀ (a b : M), a * b = b * a

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

Instances

@[instance]

def comm_monoid.to_monoid (M : Type u) [self : comm_monoid M] :

@[instance]

def add_left_cancel_monoid.to_add_monoid (M : Type u) [self : add_left_cancel_monoid M] :

@[class]

structure add_left_cancel_monoid (M : 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
nsmul : ℕ → M → M
nsmul_zero' : (∀ (x : M), add_left_cancel_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : M), add_left_cancel_monoid.nsmul n.succ x = x + add_left_cancel_monoid.nsmul n x) . "try_refl_tac"

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

@[instance]

def add_left_cancel_monoid.to_add_left_cancel_semigroup (M : Type u) [self : add_left_cancel_monoid M] :

add_left_cancel_semigroup M

@[class]

structure left_cancel_monoid (M : 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
npow : ℕ → M → M
npow_zero' : (∀ (x : M), left_cancel_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M), left_cancel_monoid.npow n.succ x = x * left_cancel_monoid.npow n x) . "try_refl_tac"

A monoid in which multiplication is left-cancellative.

Instances

@[instance]

def left_cancel_monoid.to_left_cancel_semigroup (M : Type u) [self : left_cancel_monoid M] :

left_cancel_semigroup M

@[instance]

def left_cancel_monoid.to_monoid (M : Type u) [self : left_cancel_monoid M] :

@[instance]

def add_right_cancel_monoid.to_add_right_cancel_semigroup (M : Type u) [self : add_right_cancel_monoid M] :

add_right_cancel_semigroup M

@[class]

structure add_right_cancel_monoid (M : 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
nsmul : ℕ → M → M
nsmul_zero' : (∀ (x : M), add_right_cancel_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : M), add_right_cancel_monoid.nsmul n.succ x = x + add_right_cancel_monoid.nsmul n x) . "try_refl_tac"

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]

def add_right_cancel_monoid.to_add_monoid (M : Type u) [self : add_right_cancel_monoid M] :

@[instance]

def right_cancel_monoid.to_monoid (M : Type u) [self : right_cancel_monoid M] :

@[class]

structure right_cancel_monoid (M : 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
npow : ℕ → M → M
npow_zero' : (∀ (x : M), right_cancel_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M), right_cancel_monoid.npow n.succ x = x * right_cancel_monoid.npow n x) . "try_refl_tac"

A monoid in which multiplication is right-cancellative.

Instances

@[instance]

def right_cancel_monoid.to_right_cancel_semigroup (M : Type u) [self : right_cancel_monoid M] :

right_cancel_semigroup M

@[instance]

def add_cancel_monoid.to_add_right_cancel_monoid (M : Type u) [self : add_cancel_monoid M] :

add_right_cancel_monoid M

@[class]

structure add_cancel_monoid (M : 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
nsmul : ℕ → M → M
nsmul_zero' : (∀ (x : M), add_cancel_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : M), add_cancel_monoid.nsmul n.succ x = x + add_cancel_monoid.nsmul n x) . "try_refl_tac"
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

@[instance]

def add_cancel_monoid.to_add_left_cancel_monoid (M : Type u) [self : add_cancel_monoid M] :

add_left_cancel_monoid M

@[instance]

def cancel_monoid.to_right_cancel_monoid (M : Type u) [self : cancel_monoid M] :

right_cancel_monoid M

@[class]

structure cancel_monoid (M : 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
npow : ℕ → M → M
npow_zero' : (∀ (x : M), cancel_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M), cancel_monoid.npow n.succ x = x * cancel_monoid.npow n x) . "try_refl_tac"
mul_right_cancel : ∀ (a b c_1 : M), a * b = c_1 * b → a = c_1

A monoid in which multiplication is cancellative.

Instances

@[instance]

def cancel_monoid.to_left_cancel_monoid (M : Type u) [self : cancel_monoid M] :

left_cancel_monoid M

@[instance]

def add_cancel_comm_monoid.to_add_left_cancel_monoid (M : Type u) [self : add_cancel_comm_monoid M] :

add_left_cancel_monoid M

@[class]

structure add_cancel_comm_monoid (M : 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
nsmul : ℕ → M → M
nsmul_zero' : (∀ (x : M), add_cancel_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : M), add_cancel_comm_monoid.nsmul n.succ x = x + add_cancel_comm_monoid.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : M), a + b = b + a

Commutative version of add_cancel_monoid.

Instances

@[instance]

def add_cancel_comm_monoid.to_add_comm_monoid (M : Type u) [self : add_cancel_comm_monoid M] :

add_comm_monoid M

@[instance]

def cancel_comm_monoid.to_comm_monoid (M : Type u) [self : cancel_comm_monoid M] :

@[class]

structure cancel_comm_monoid (M : 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
npow : ℕ → M → M
npow_zero' : (∀ (x : M), cancel_comm_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M), cancel_comm_monoid.npow n.succ x = x * cancel_comm_monoid.npow n x) . "try_refl_tac"
mul_comm : ∀ (a b : M), a * b = b * a

Commutative version of cancel_monoid.

Instances

@[instance]

def cancel_comm_monoid.to_left_cancel_monoid (M : Type u) [self : cancel_comm_monoid M] :

left_cancel_monoid M

@[instance]

def cancel_comm_monoid.to_cancel_monoid (M : Type u) [cancel_comm_monoid M] :

cancel_monoid M

Equations

cancel_comm_monoid.to_cancel_monoid M = {mul := cancel_comm_monoid.mul _inst_1, mul_assoc := _, mul_left_cancel := _, one := cancel_comm_monoid.one _inst_1, one_mul := _, mul_one := _, npow := cancel_comm_monoid.npow _inst_1, npow_zero' := _, npow_succ' := _, mul_right_cancel := _}

@[instance]

def add_cancel_comm_monoid.to_cancel_add_monoid (M : Type u) [add_cancel_comm_monoid M] :

add_cancel_monoid M

def gpow_rec {M : Type u_1} [has_one M] [has_mul M] [has_inv M] :

ℤ → M → M

The fundamental power operation in a group. gpow_rec n a = a*a*...*a n times, for integer n. Use instead a ^ n, which has better definitional behavior.

Equations

gpow_rec -[1+ n] a = (npow_rec n.succ a)⁻¹
gpow_rec (int.of_nat n) a = npow_rec n a

def gsmul_rec {M : Type u_1} [has_zero M] [has_add M] [has_neg M] :

ℤ → M → M

The fundamental scalar multiplication in an additive group. gsmul_rec n a = a+a+...+a n times, for integer n. Use instead n • a, which has better definitional behavior.

Equations

gsmul_rec -[1+ n] a = -nsmul_rec n.succ a
gsmul_rec (int.of_nat n) a = nsmul_rec n a

@[instance]

def div_inv_monoid.to_monoid (G : Type u) [self : div_inv_monoid G] :

@[instance]

def div_inv_monoid.to_has_div (G : Type u) [self : div_inv_monoid G] :

@[class]

structure div_inv_monoid (G : 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
npow : ℕ → G → G
npow_zero' : (∀ (x : G), div_inv_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : G), div_inv_monoid.npow n.succ x = x * div_inv_monoid.npow n x) . "try_refl_tac"
inv : G → G
div : G → G → G
div_eq_mul_inv : (∀ (a b : G), a / b = a * b⁻¹) . "try_refl_tac"
gpow : ℤ → G → G
gpow_zero' : (∀ (a : G), gpow 0 a = 1) . "try_refl_tac"
gpow_succ' : (∀ (n : ℕ) (a : G), gpow (int.of_nat n.succ) a = a * gpow (int.of_nat n) a) . "try_refl_tac"
gpow_neg' : (∀ (n : ℕ) (a : G), gpow -[1+ n] a = (gpow ↑(n.succ) a)⁻¹) . "try_refl_tac"

A div_inv_monoid is a monoid with operations / and ⁻¹ satisfying div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹.

This is the immediate common ancestor of group and group_with_zero, in order to deduplicate the name div_eq_mul_inv. The default for div is such that a / b = a * b⁻¹ holds by definition.

Adding div as a field rather than defining a / b := a * b⁻¹ allows us to avoid certain classes of unification failures, for example: Let foo X be a type with a ∀ X, has_div (foo X) instance but no ∀ X, has_inv (foo X), e.g. when foo X is a euclidean_domain. Suppose we also have an instance ∀ X [cromulent X], group_with_zero (foo X). Then the (/) coming from group_with_zero_has_div cannot be definitionally equal to the (/) coming from foo.has_div.

In the same way, adding a gpow field makes it possible to avoid definitional failures in diamonds. See the definition of monoid and Note [forgetful inheritance] for more explanations on this.

Instances

@[instance]

def div_inv_monoid.to_has_inv (G : Type u) [self : div_inv_monoid G] :

@[instance]

def sub_neg_monoid.to_has_sub (G : Type u) [self : sub_neg_monoid G] :

@[instance]

def sub_neg_monoid.to_add_monoid (G : Type u) [self : sub_neg_monoid G] :

@[class]

structure sub_neg_monoid (G : 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
nsmul : ℕ → G → G
nsmul_zero' : (∀ (x : G), sub_neg_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : G), sub_neg_monoid.nsmul n.succ x = x + sub_neg_monoid.nsmul n x) . "try_refl_tac"
neg : G → G
sub : G → G → G
sub_eq_add_neg : (∀ (a b : G), a - b = a + -b) . "try_refl_tac"
gsmul : ℤ → G → G
gsmul_zero' : (∀ (a : G), gsmul 0 a = 0) . "try_refl_tac"
gsmul_succ' : (∀ (n : ℕ) (a : G), gsmul (int.of_nat n.succ) a = a + gsmul (int.of_nat n) a) . "try_refl_tac"
gsmul_neg' : (∀ (n : ℕ) (a : G), gsmul -[1+ n] a = -gsmul ↑(n.succ) a) . "try_refl_tac"

A sub_neg_monoid is an add_monoid with unary - and binary - operations satisfying sub_eq_add_neg : ∀ a b, a - b = a + -b.

The default for sub is such that a - b = a + -b holds by definition.

Adding sub as a field rather than defining a - b := a + -b allows us to avoid certain classes of unification failures, for example: Let foo X be a type with a ∀ X, has_sub (foo X) instance but no ∀ X, has_neg (foo X). Suppose we also have an instance ∀ X [cromulent X], add_group (foo X). Then the (-) coming from add_group.has_sub cannot be definitionally equal to the (-) coming from foo.has_sub.

In the same way, adding a gsmul field makes it possible to avoid definitional failures in diamonds. See the definition of add_monoid and Note [forgetful inheritance] for more explanations on this.

Instances

@[instance]

def sub_neg_monoid.to_has_neg (G : Type u) [self : sub_neg_monoid G] :

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

a / b = a * b⁻¹

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

a - b = a + -b

@[class]

structure group (G : 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
npow : ℕ → G → G
npow_zero' : (∀ (x : G), group.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : G), group.npow n.succ x = x * group.npow n x) . "try_refl_tac"
inv : G → G
div : G → G → G
div_eq_mul_inv : (∀ (a b : G), a / b = a * b⁻¹) . "try_refl_tac"
gpow : ℤ → G → G
gpow_zero' : (∀ (a : G), group.gpow 0 a = 1) . "try_refl_tac"
gpow_succ' : (∀ (n : ℕ) (a : G), group.gpow (int.of_nat n.succ) a = a * group.gpow (int.of_nat n) a) . "try_refl_tac"
gpow_neg' : (∀ (n : ℕ) (a : G), group.gpow -[1+ n] a = (group.gpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1

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

There is also a division operation / such that a / b = a * b⁻¹, with a default so that a / b = a * b⁻¹ holds by definition.

Instances

@[instance]

def group.to_div_inv_monoid (G : Type u) [self : group G] :

div_inv_monoid G

@[class]

structure add_group (A : Type u) :

Type u

add : A → A → A
add_assoc : ∀ (a b c_1 : A), a + b + c_1 = a + (b + c_1)
zero : A
zero_add : ∀ (a : A), 0 + a = a
add_zero : ∀ (a : A), a + 0 = a
nsmul : ℕ → A → A
nsmul_zero' : (∀ (x : A), add_group.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : A), add_group.nsmul n.succ x = x + add_group.nsmul n x) . "try_refl_tac"
neg : A → A
sub : A → A → A
sub_eq_add_neg : (∀ (a b : A), a - b = a + -b) . "try_refl_tac"
gsmul : ℤ → A → A
gsmul_zero' : (∀ (a : A), add_group.gsmul 0 a = 0) . "try_refl_tac"
gsmul_succ' : (∀ (n : ℕ) (a : A), add_group.gsmul (int.of_nat n.succ) a = a + add_group.gsmul (int.of_nat n) a) . "try_refl_tac"
gsmul_neg' : (∀ (n : ℕ) (a : A), add_group.gsmul -[1+ n] a = -add_group.gsmul ↑(n.succ) a) . "try_refl_tac"
add_left_neg : ∀ (a : A), -a + a = 0

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

There is also a binary operation - such that a - b = a + -b, with a default so that a - b = a + -b holds by definition.

Instances

@[instance]

def add_group.to_sub_neg_monoid (A : Type u) [self : add_group A] :

sub_neg_monoid A

def add_group.to_add_monoid (G : Type u) [add_group G] :

Abbreviation for @sub_neg_monoid.to_add_monoid _ (@add_group.to_sub_neg_monoid _ _).

Useful because it corresponds to the fact that AddGroup is a subcategory of AddMon. Not an instance since it duplicates @sub_neg_monoid.to_add_monoid _ (@add_group.to_sub_neg_monoid _ _).

def group.to_monoid (G : Type u) [group G] :

Abbreviation for @div_inv_monoid.to_monoid _ (@group.to_div_inv_monoid _ _).

Useful because it corresponds to the fact that Grp is a subcategory of Mon. Not an instance since it duplicates @div_inv_monoid.to_monoid _ (@group.to_div_inv_monoid _ _).

Equations

group.to_monoid G = div_inv_monoid.to_monoid G

@[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} (h : a * b = 1) :

@[simp]

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

-a = b

@[simp]

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

a⁻¹ ⁻¹ = a

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

cancel_monoid G

Equations

group.to_cancel_monoid = {mul := group.mul _inst_1, mul_assoc := _, mul_left_cancel := _, one := group.one _inst_1, one_mul := _, mul_one := _, npow := group.npow _inst_1, npow_zero' := _, npow_succ' := _, mul_right_cancel := _}

@[instance]

def add_group.to_cancel_add_monoid {G : Type u} [add_group G] :

add_cancel_monoid G

@[instance]

def comm_group.to_group (G : Type u) [self : comm_group G] :

@[class]

structure comm_group (G : 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
npow : ℕ → G → G
npow_zero' : (∀ (x : G), comm_group.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : G), comm_group.npow n.succ x = x * comm_group.npow n x) . "try_refl_tac"
inv : G → G
div : G → G → G
div_eq_mul_inv : (∀ (a b : G), a / b = a * b⁻¹) . "try_refl_tac"
gpow : ℤ → G → G
gpow_zero' : (∀ (a : G), comm_group.gpow 0 a = 1) . "try_refl_tac"
gpow_succ' : (∀ (n : ℕ) (a : G), comm_group.gpow (int.of_nat n.succ) a = a * comm_group.gpow (int.of_nat n) a) . "try_refl_tac"
gpow_neg' : (∀ (n : ℕ) (a : G), comm_group.gpow -[1+ n] a = (comm_group.gpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
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) [self : comm_group G] :

@[class]

structure add_comm_group (G : 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
nsmul : ℕ → G → G
nsmul_zero' : (∀ (x : G), add_comm_group.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : G), add_comm_group.nsmul n.succ x = x + add_comm_group.nsmul n x) . "try_refl_tac"
neg : G → G
sub : G → G → G
sub_eq_add_neg : (∀ (a b : G), a - b = a + -b) . "try_refl_tac"
gsmul : ℤ → G → G
gsmul_zero' : (∀ (a : G), add_comm_group.gsmul 0 a = 0) . "try_refl_tac"
gsmul_succ' : (∀ (n : ℕ) (a : G), add_comm_group.gsmul (int.of_nat n.succ) a = a + add_comm_group.gsmul (int.of_nat n) a) . "try_refl_tac"
gsmul_neg' : (∀ (n : ℕ) (a : G), add_comm_group.gsmul -[1+ n] a = -add_comm_group.gsmul ↑(n.succ) a) . "try_refl_tac"
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]

def add_comm_group.to_add_comm_monoid (G : Type u) [self : add_comm_group G] :

add_comm_monoid G

@[instance]

def add_comm_group.to_add_group (G : Type u) [self : add_comm_group G] :

@[instance]

def comm_group.to_cancel_comm_monoid {G : Type u} [comm_group G] :

cancel_comm_monoid G

Equations

comm_group.to_cancel_comm_monoid = {mul := comm_group.mul _inst_1, mul_assoc := _, mul_left_cancel := _, one := comm_group.one _inst_1, one_mul := _, mul_one := _, npow := comm_group.npow _inst_1, npow_zero' := _, npow_succ' := _, mul_comm := _}

@[instance]

def add_comm_group.to_cancel_add_comm_monoid {G : Type u} [add_comm_group G] :

add_cancel_comm_monoid G