mathlib documentation

algebra.group.defs

Typeclasses for (semi)groups and monoids #

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.

We also introduce notation classes has_smul and has_vadd for multiplicative and additive actions and register the following instances:

has_pow M ℕ, for monoids M, and has_pow G ℤ for groups G;
has_smul ℕ M for additive monoids M, and has_smul ℤ G for additive groups G.

Notation #

+, -, *, /, ^ : the usual arithmetic operations; the underlying functions are has_add.add, has_neg.neg/has_sub.sub, has_mul.mul, has_div.div, and has_pow.pow.
a • b is used as notation for has_smul.smul a b.
a +ᵥ b is used as notation for has_vadd.vadd a b.

@[class]

structure has_vadd (G : Type u_1) (P : Type u_2) :

Type (max u_1 u_2)

vadd : G → P → P

Type class for the +ᵥ notation.

Instances of this typeclass

Instances of other typeclasses for has_vadd

has_vadd.has_sizeof_inst

@[class]

structure has_vsub (G : out_param (Type u_1)) (P : Type u_2) :

Type (max u_1 u_2)

vsub : P → P → G

Type class for the -ᵥ notation.

Instances of this typeclass

Instances of other typeclasses for has_vsub

has_vsub.has_sizeof_inst

theorem has_smul.ext {M : Type u_1} {α : Type u_2} (x y : has_smul M α) (h : has_smul.smul = has_smul.smul) :

x = y

theorem has_smul.ext_iff {M : Type u_1} {α : Type u_2} (x y : has_smul M α) :

x = y ↔ has_smul.smul = has_smul.smul

@[ext, class]

structure has_smul (M : Type u_1) (α : Type u_2) :

Type (max u_1 u_2)

smul : M → α → α

Typeclass for types with a scalar multiplication operation, denoted • (\bu)

Instances of this typeclass

Instances of other typeclasses for has_smul

has_smul.has_sizeof_inst

meta def simp_attr.field_simps :

(user_attribute simp_lemmas)

The simpset field_simps is used by the tactic field_simp to reduce an expression in a field to an expression of the form n / d where n and d are division-free.

def left_mul {G : Type u_1} [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_1} [has_add G] :

G → G → G

left_add g denotes left addition by g

Equations

left_add = λ (g x : G), g + x

def right_add {G : Type u_1} [has_add G] :

G → G → G

right_add g denotes right addition by g

Equations

right_add = λ (g x : G), x + g

def right_mul {G : Type u_1} [has_mul G] :

G → G → G

right_mul g denotes right multiplication by g

Equations

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

theorem semigroup.ext_iff {G : Type u} (x y : semigroup G) :

x = y ↔ semigroup.mul = semigroup.mul

theorem semigroup.ext {G : Type u} (x y : semigroup G) (h : semigroup.mul = semigroup.mul) :

x = y

@[instance]

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

Instances for semigroup.to_has_mul

Semigroup.semigroup.to_has_mul.category_theory.bundled_hom.parent_projection

@[ext, class]

structure semigroup (G : Type u) :

Type u

mul : G → G → G
mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)

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

Instances of this typeclass

Instances of other typeclasses for semigroup

semigroup.has_sizeof_inst

@[instance]

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

Instances for add_semigroup.to_has_add

AddSemigroup.semigroup.to_has_mul.category_theory.bundled_hom.parent_projection

theorem add_semigroup.ext_iff {G : Type u} (x y : add_semigroup G) :

x = y ↔ add_semigroup.add = add_semigroup.add

theorem add_semigroup.ext {G : Type u} (x y : add_semigroup G) (h : add_semigroup.add = add_semigroup.add) :

x = y

@[ext, class]

structure add_semigroup (G : Type u) :

Type u

add : G → G → G
add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)

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

Instances of this typeclass

Instances of other typeclasses for add_semigroup

add_semigroup.has_sizeof_inst

theorem add_assoc {G : Type u_1} [add_semigroup G] (a b c : G) :

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

theorem mul_assoc {G : Type u_1} [semigroup G] (a b c : G) :

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

@[protected, instance]

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

is_associative G has_add.add

@[protected, instance]

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

is_associative G has_mul.mul

@[ext, class]

structure comm_semigroup (G : Type u) :

Type u

mul : G → G → G
mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_comm : ∀ (a b : G), a * b = b * a

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

Instances of this typeclass

Instances of other typeclasses for comm_semigroup

comm_semigroup.has_sizeof_inst

@[instance]

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

theorem comm_semigroup.ext_iff {G : Type u} (x y : comm_semigroup G) :

x = y ↔ comm_semigroup.mul = comm_semigroup.mul

theorem comm_semigroup.ext {G : Type u} (x y : comm_semigroup G) (h : comm_semigroup.mul = comm_semigroup.mul) :

x = y

theorem add_comm_semigroup.ext_iff {G : Type u} (x y : add_comm_semigroup G) :

x = y ↔ add_comm_semigroup.add = add_comm_semigroup.add

@[instance]

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

add_semigroup G

theorem add_comm_semigroup.ext {G : Type u} (x y : add_comm_semigroup G) (h : add_comm_semigroup.add = add_comm_semigroup.add) :

x = y

@[ext, class]

structure add_comm_semigroup (G : Type u) :

Type u

add : G → G → G
add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
add_comm : ∀ (a b : G), a + b = b + a

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

Instances of this typeclass

Instances of other typeclasses for add_comm_semigroup

add_comm_semigroup.has_sizeof_inst

theorem add_comm {G : Type u_1} [add_comm_semigroup G] (a b : G) :

a + b = b + a

theorem mul_comm {G : Type u_1} [comm_semigroup G] (a b : G) :

a * b = b * a

@[protected, instance]

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

is_commutative G has_mul.mul

@[protected, instance]

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

is_commutative G has_add.add

theorem left_cancel_semigroup.ext {G : Type u} (x y : left_cancel_semigroup G) (h : left_cancel_semigroup.mul = left_cancel_semigroup.mul) :

x = y

@[instance]

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

@[ext, class]

structure left_cancel_semigroup (G : Type u) :

Type u

mul : G → G → G
mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_left_cancel : ∀ (a b c : G), a * b = a * c → b = c

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

Instances of this typeclass

Instances of other typeclasses for left_cancel_semigroup

left_cancel_semigroup.has_sizeof_inst

theorem left_cancel_semigroup.ext_iff {G : Type u} (x y : left_cancel_semigroup G) :

x = y ↔ left_cancel_semigroup.mul = left_cancel_semigroup.mul

@[ext, class]

structure add_left_cancel_semigroup (G : Type u) :

Type u

add : G → G → G
add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
add_left_cancel : ∀ (a b c : G), a + b = a + c → b = c

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

Instances of this typeclass

Instances of other typeclasses for add_left_cancel_semigroup

add_left_cancel_semigroup.has_sizeof_inst

theorem add_left_cancel_semigroup.ext_iff {G : Type u} (x y : add_left_cancel_semigroup G) :

x = y ↔ add_left_cancel_semigroup.add = add_left_cancel_semigroup.add

@[instance]

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

add_semigroup G

theorem add_left_cancel_semigroup.ext {G : Type u} (x y : add_left_cancel_semigroup G) (h : add_left_cancel_semigroup.add = add_left_cancel_semigroup.add) :

x = y

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

a * b = a * c → b = c

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

a + b = a + c → b = c

theorem add_left_cancel_iff {G : Type u_1} [add_left_cancel_semigroup G] {a b c : G} :

a + b = a + c ↔ b = c

theorem mul_left_cancel_iff {G : Type u_1} [left_cancel_semigroup G] {a b c : G} :

a * b = a * c ↔ b = c

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

function.injective (has_add.add a)

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

function.injective (has_mul.mul a)

@[simp]

theorem mul_right_inj {G : Type u_1} [left_cancel_semigroup G] (a : G) {b c : G} :

a * b = a * c ↔ b = c

@[simp]

theorem add_right_inj {G : Type u_1} [add_left_cancel_semigroup G] (a : G) {b c : G} :

a + b = a + c ↔ b = c

theorem mul_ne_mul_right {G : Type u_1} [left_cancel_semigroup G] (a : G) {b c : G} :

a * b ≠ a * c ↔ b ≠ c

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

a + b ≠ a + c ↔ b ≠ c

theorem right_cancel_semigroup.ext {G : Type u} (x y : right_cancel_semigroup G) (h : right_cancel_semigroup.mul = right_cancel_semigroup.mul) :

x = y

@[ext, class]

structure right_cancel_semigroup (G : Type u) :

Type u

mul : G → G → G
mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_right_cancel : ∀ (a b c : G), a * b = c * b → a = c

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

Instances of this typeclass

Instances of other typeclasses for right_cancel_semigroup

right_cancel_semigroup.has_sizeof_inst

theorem right_cancel_semigroup.ext_iff {G : Type u} (x y : right_cancel_semigroup G) :

x = y ↔ right_cancel_semigroup.mul = right_cancel_semigroup.mul

@[instance]

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

theorem add_right_cancel_semigroup.ext {G : Type u} (x y : add_right_cancel_semigroup G) (h : add_right_cancel_semigroup.add = add_right_cancel_semigroup.add) :

x = y

theorem add_right_cancel_semigroup.ext_iff {G : Type u} (x y : add_right_cancel_semigroup G) :

x = y ↔ add_right_cancel_semigroup.add = add_right_cancel_semigroup.add

@[ext, class]

structure add_right_cancel_semigroup (G : Type u) :

Type u

add : G → G → G
add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
add_right_cancel : ∀ (a b c : G), a + b = c + b → a = c

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

Instances of this typeclass

Instances of other typeclasses for add_right_cancel_semigroup

add_right_cancel_semigroup.has_sizeof_inst

@[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_1} [right_cancel_semigroup G] {a b c : G} :

a * b = c * b → a = c

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

a + b = c + b → a = c

theorem mul_right_cancel_iff {G : Type u_1} [right_cancel_semigroup G] {a b c : G} :

b * a = c * a ↔ b = c

theorem add_right_cancel_iff {G : Type u_1} [add_right_cancel_semigroup G] {a b c : G} :

b + a = c + a ↔ b = c

theorem add_left_injective {G : Type u_1} [add_right_cancel_semigroup G] (a : G) :

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

theorem mul_left_injective {G : Type u_1} [right_cancel_semigroup G] (a : G) :

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

@[simp]

theorem add_left_inj {G : Type u_1} [add_right_cancel_semigroup G] (a : G) {b c : G} :

b + a = c + a ↔ b = c

@[simp]

theorem mul_left_inj {G : Type u_1} [right_cancel_semigroup G] (a : G) {b c : G} :

b * a = c * a ↔ b = c

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

b * a ≠ c * a ↔ b ≠ c

theorem add_ne_add_left {G : Type u_1} [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 of this typeclass

Instances of other typeclasses for mul_one_class

mul_one_class.has_sizeof_inst

@[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 of this typeclass

Instances of other typeclasses for add_zero_class

add_zero_class.has_sizeof_inst

@[ext]

theorem mul_one_class.ext {M : Type u} ⦃m₁ m₂ : mul_one_class M⦄ :

mul_one_class.mul = mul_one_class.mul → m₁ = m₂

@[ext]

theorem add_zero_class.ext {M : Type u} ⦃m₁ m₂ : add_zero_class M⦄ :

add_zero_class.add = add_zero_class.add → m₁ = m₂

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

@[protected, instance]

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

is_left_id M has_mul.mul 1

@[protected, instance]

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

is_left_id M has_add.add 0

@[protected, instance]

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

is_right_id M has_mul.mul 1

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

def library_note.forgetful inheritance :

Suppose that one can put two mathematical structures on a type, a rich one R and a poor one P, and that one can deduce the poor structure from the rich structure through a map F (called a forgetful functor) (think R = metric_space and P = topological_space). A possible implementation would be to have a type class rich containing a field R, a type class poor containing a field P, and an instance from rich to poor. However, this creates diamond problems, and a better approach is to let rich extend poor and have a field saying that F R = P.

To illustrate this, consider the pair metric_space / topological_space. Consider the topology on a product of two metric spaces. With the first approach, it could be obtained by going first from each metric space to its topology, and then taking the product topology. But it could also be obtained by considering the product metric space (with its sup distance) and then the topology coming from this distance. These would be the same topology, but not definitionally, which means that from the point of view of Lean's kernel, there would be two different topological_space instances on the product. This is not compatible with the way instances are designed and used: there should be at most one instance of a kind on each type. This approach has created an instance diamond that does not commute definitionally.

The second approach solves this issue. Now, a metric space contains both a distance, a topology, and a proof that the topology coincides with the one coming from the distance. When one defines the product of two metric spaces, one uses the sup distance and the product topology, and one has to give the proof that the sup distance induces the product topology. Following both sides of the instance diamond then gives rise (definitionally) to the product topology on the product space.

Another approach would be to have the rich type class take the poor type class as an instance parameter. It would solve the diamond problem, but it would lead to a blow up of the number of type classes one would need to declare to work with complicated classes, say a real inner product space, and would create exponential complexity when working with products of such complicated spaces, that are avoided by bundling things carefully as above.

Note that this description of this specific case of the product of metric spaces is oversimplified compared to mathlib, as there is an intermediate typeclass between metric_space and topological_space called uniform_space. The above scheme is used at both levels, embedding a topology in the uniform space structure, and a uniform structure in the metric space structure.

Note also that, when P is a proposition, there is no such issue as any two proofs of P are definitionally equivalent in Lean.

To avoid boilerplate, there are some designs that can automatically fill the poor fields when creating a rich structure if one doesn't want to do something special about them. For instance, in the definition of metric spaces, default tactics fill the uniform space fields if they are not given explicitly. One can also have a helper function creating the rich structure from a structure with fewer fields, where the helper function fills the remaining fields. See for instance uniform_space.of_core or real_inner_product.of_core.

For more details on this question, called the forgetful inheritance pattern, see Competing inheritance paths in dependent type theory: a case study in functional analysis.

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_smul ℕ α 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_smul ℕ (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.

A basic theory for the power function on monoids and the ℕ-action on additive monoids is 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 : M), a + b + c = a + (b + c)
zero : M
zero_add : ∀ (a : M), 0 + a = a
add_zero : ∀ (a : M), a + 0 = a
nsmul : ℕ → M → M
nsmul_zero' : (∀ (x : M), add_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : M), add_monoid.nsmul n.succ x = x + add_monoid.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 of this typeclass

Instances of other typeclasses for add_monoid

add_monoid.has_sizeof_inst

@[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 : M), a * b * c = a * (b * c)
one : M
one_mul : ∀ (a : M), 1 * a = a
mul_one : ∀ (a : M), a * 1 = a
npow : ℕ → M → M
npow_zero' : (∀ (x : M), monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : M), monoid.npow n.succ x = x * monoid.npow n x) . "try_refl_tac"

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

Instances of this typeclass

Instances of other typeclasses for monoid

monoid.has_sizeof_inst

@[protected, instance]

def monoid.has_pow {M : Type u_1} [monoid M] :

Equations

monoid.has_pow = {pow := λ (x : M) (n : ℕ), monoid.npow n x}

@[protected, instance]

def add_monoid.has_smul_nat {M : Type u_1} [add_monoid M] :

Equations

add_monoid.has_smul_nat = {smul := add_monoid.nsmul _inst_1}

@[simp]

theorem npow_eq_pow {M : Type u_2} [monoid M] (n : ℕ) (x : M) :

monoid.npow n x = x ^ n

@[simp]

theorem nsmul_eq_smul {M : Type u_2} [add_monoid M] (n : ℕ) (x : M) :

add_monoid.nsmul n x = n • x

theorem zero_nsmul {M : Type u_2} [add_monoid M] (a : M) :

0 • a = 0

@[simp]

theorem pow_zero {M : Type u_2} [monoid M] (a : M) :

a ^ 0 = 1

theorem succ_nsmul {M : Type u_2} [add_monoid M] (a : M) (n : ℕ) :

(n + 1) • a = a + n • a

theorem pow_succ {M : Type u_2} [monoid M] (a : M) (n : ℕ) :

a ^ (n + 1) = a * a ^ n

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

@[instance]

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

Instances for add_comm_monoid.to_add_monoid

AddCommMon.comm_monoid.to_monoid.category_theory.bundled_hom.parent_projection

@[class]

structure add_comm_monoid (M : Type u) :

Type u

add : M → M → M
add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)
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 of this typeclass

Instances of other typeclasses for add_comm_monoid

add_comm_monoid.has_sizeof_inst

@[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 : M), a * b * c = a * (b * c)
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 of this typeclass

Instances of other typeclasses for comm_monoid

comm_monoid.has_sizeof_inst

@[instance]

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

Instances for comm_monoid.to_monoid

CommMon.comm_monoid.to_monoid.category_theory.bundled_hom.parent_projection

@[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 : M), a + b + c = a + (b + c)
add_left_cancel : ∀ (a b c : M), a + b = a + c → b = c
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 of this typeclass

Instances of other typeclasses for add_left_cancel_monoid

add_left_cancel_monoid.has_sizeof_inst

@[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 : M), a * b * c = a * (b * c)
mul_left_cancel : ∀ (a b c : M), a * b = a * c → b = c
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 of this typeclass

Instances of other typeclasses for left_cancel_monoid

left_cancel_monoid.has_sizeof_inst

@[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 : M), a + b + c = a + (b + c)
add_right_cancel : ∀ (a b c : M), a + b = c + b → a = c
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 of this typeclass

Instances of other typeclasses for add_right_cancel_monoid

add_right_cancel_monoid.has_sizeof_inst

@[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 : M), a * b * c = a * (b * c)
mul_right_cancel : ∀ (a b c : M), a * b = c * b → a = c
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 of this typeclass

Instances of other typeclasses for right_cancel_monoid

right_cancel_monoid.has_sizeof_inst

@[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 : M), a + b + c = a + (b + c)
add_left_cancel : ∀ (a b c : M), a + b = a + c → b = c
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 : M), a + b = c + b → a = c

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 of this typeclass

Instances of other typeclasses for add_cancel_monoid

add_cancel_monoid.has_sizeof_inst

@[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 : M), a * b * c = a * (b * c)
mul_left_cancel : ∀ (a b c : M), a * b = a * c → b = c
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 : M), a * b = c * b → a = c

A monoid in which multiplication is cancellative.

Instances of this typeclass

Instances of other typeclasses for cancel_monoid

cancel_monoid.has_sizeof_inst

@[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 : M), a + b + c = a + (b + c)
add_left_cancel : ∀ (a b c : M), a + b = a + c → b = c
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 of this typeclass

Instances of other typeclasses for add_cancel_comm_monoid

add_cancel_comm_monoid.has_sizeof_inst

@[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 : M), a * b * c = a * (b * c)
mul_left_cancel : ∀ (a b c : M), a * b = a * c → b = c
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 of this typeclass

Instances of other typeclasses for cancel_comm_monoid

cancel_comm_monoid.has_sizeof_inst

@[instance]

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

left_cancel_monoid M

@[protected, 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 := _}

@[protected, instance]

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

add_cancel_monoid M

Equations

add_cancel_comm_monoid.to_cancel_add_monoid M = {add := add_cancel_comm_monoid.add _inst_1, add_assoc := _, add_left_cancel := _, zero := add_cancel_comm_monoid.zero _inst_1, zero_add := _, add_zero := _, nsmul := add_cancel_comm_monoid.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_right_cancel := _}

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

ℤ → M → M

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

Equations

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

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

ℤ → M → M

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

Equations

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

@[class]

structure has_involutive_neg (A : Type u_2) :

Type u_2

neg : A → A
neg_neg : ∀ (x : A), --x = x

Auxiliary typeclass for types with an involutive has_neg.

Instances of this typeclass

Instances of other typeclasses for has_involutive_neg

has_involutive_neg.has_sizeof_inst

@[instance]

def has_involutive_neg.to_has_neg (A : Type u_2) [self : has_involutive_neg A] :

@[class]

structure has_involutive_inv (G : Type u_2) :

Type u_2

inv : G → G
inv_inv : ∀ (x : G), x⁻¹ ⁻¹ = x

Auxiliary typeclass for types with an involutive has_inv.

Instances of this typeclass

Instances of other typeclasses for has_involutive_inv

has_involutive_inv.has_sizeof_inst

@[instance]

def has_involutive_inv.to_has_inv (G : Type u_2) [self : has_involutive_inv G] :

@[simp]

theorem inv_inv {G : Type u_1} [has_involutive_inv G] (a : G) :

a⁻¹ ⁻¹ = a

@[simp]

theorem neg_neg {G : Type u_1} [has_involutive_neg G] (a : G) :

--a = a

Design note on `div_inv_monoid`/`sub_neg_monoid` and `division_monoid`/`subtraction_monoid` #

Those two pairs of made-up classes fulfill slightly different roles.

div_inv_monoid/sub_neg_monoid provides the minimum amount of information to define the ℤ action (zpow or zsmul). Further, it provides a div field, matching the forgetful inheritance pattern. This is useful to shorten extension clauses of stronger structures (group, group_with_zero, division_ring, field) and for a few structures with a rather weak pseudo-inverse (matrix).

division_monoid/subtraction_monoid is targeted at structures with stronger pseudo-inverses. It is an ad hoc collection of axioms that are mainly respected by three things:

Groups
Groups with zero
The pointwise monoids set α, finset α, filter α

It acts as a middle ground for structures with an inversion operator that plays well with multiplication, except for the fact that it might not be a true inverse (a / a ≠ 1 in general). The axioms are pretty arbitrary (many other combinations are equivalent to it), but they are independent:

Without division_monoid.div_eq_mul_inv, you can define / arbitrarily.
Without division_monoid.inv_inv, you can consider with_top unit with a⁻¹ = ⊤ for all a.
Without division_monoid.mul_inv_rev, you can consider with_top α with a⁻¹ = a for all a where α non commutative.
Without division_monoid.inv_eq_of_mul, you can consider any comm_monoid with a⁻¹ = a for all a.

As a consequence, a few natural structures do not fit in this framework. For example, ennreal respects everything except for the fact that (0 * ∞)⁻¹ = 0⁻¹ = ∞ while ∞⁻¹ * 0⁻¹ = 0 * ∞ = 0.

@[instance]

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

Instances for div_inv_monoid.to_monoid

Group.group.to_monoid.category_theory.bundled_hom.parent_projection

@[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 : G), a * b * c = a * (b * c)
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"
zpow : ℤ → G → G
zpow_zero' : (∀ (a : G), div_inv_monoid.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : G), div_inv_monoid.zpow (int.of_nat n.succ) a = a * div_inv_monoid.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : G), div_inv_monoid.zpow -[1+ n] a = (div_inv_monoid.zpow ↑(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 deduplicates 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 zpow 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 of this typeclass

Instances of other typeclasses for div_inv_monoid

div_inv_monoid.has_sizeof_inst

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

Instances for sub_neg_monoid.to_add_monoid

AddGroup.group.to_monoid.category_theory.bundled_hom.parent_projection

@[class]

structure sub_neg_monoid (G : Type u) :

Type u

add : G → G → G
add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
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"
zsmul : ℤ → G → G
zsmul_zero' : (∀ (a : G), sub_neg_monoid.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : G), sub_neg_monoid.zsmul (int.of_nat n.succ) a = a + sub_neg_monoid.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : G), sub_neg_monoid.zsmul -[1+ n] a = -sub_neg_monoid.zsmul ↑(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 zsmul 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 of this typeclass

Instances of other typeclasses for sub_neg_monoid

sub_neg_monoid.has_sizeof_inst

@[instance]

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

@[protected, instance]

def div_inv_monoid.has_pow {M : Type u_1} [div_inv_monoid M] :

Equations

div_inv_monoid.has_pow = {pow := λ (x : M) (n : ℤ), div_inv_monoid.zpow n x}

@[protected, instance]

def sub_neg_monoid.has_smul_int {M : Type u_1} [sub_neg_monoid M] :

Equations

sub_neg_monoid.has_smul_int = {smul := sub_neg_monoid.zsmul _inst_1}

@[simp]

theorem zsmul_eq_smul {G : Type u_1} [sub_neg_monoid G] (n : ℤ) (x : G) :

sub_neg_monoid.zsmul n x = n • x

@[simp]

theorem zpow_eq_pow {G : Type u_1} [div_inv_monoid G] (n : ℤ) (x : G) :

div_inv_monoid.zpow n x = x ^ n

@[simp]

theorem zero_zsmul {G : Type u_1} [sub_neg_monoid G] (a : G) :

0 • a = 0

@[simp]

theorem zpow_zero {G : Type u_1} [div_inv_monoid G] (a : G) :

a ^ 0 = 1

@[simp, norm_cast]

theorem coe_nat_zsmul {G : Type u_1} [sub_neg_monoid G] (a : G) (n : ℕ) :

↑n • a = n • a

@[simp, norm_cast]

theorem zpow_coe_nat {G : Type u_1} [div_inv_monoid G] (a : G) (n : ℕ) :

a ^ ↑n = a ^ n

theorem of_nat_zsmul {G : Type u_1} [sub_neg_monoid G] (a : G) (n : ℕ) :

int.of_nat n • a = n • a

theorem zpow_of_nat {G : Type u_1} [div_inv_monoid G] (a : G) (n : ℕ) :

a ^ int.of_nat n = a ^ n

@[simp]

theorem zsmul_neg_succ_of_nat {G : Type u_1} [sub_neg_monoid G] (a : G) (n : ℕ) :

-[1+ n] • a = -((n + 1) • a)

@[simp]

theorem zpow_neg_succ_of_nat {G : Type u_1} [div_inv_monoid G] (a : G) (n : ℕ) :

a ^ -[1+ n] = (a ^ (n + 1))⁻¹

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

a / b = a * b⁻¹

Dividing by an element is the same as multiplying by its inverse.

This is a duplicate of div_inv_monoid.div_eq_mul_inv ensuring that the types unfold better.

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

a - b = a + -b

Subtracting an element is the same as adding by its negative.

This is a duplicate of sub_neg_monoid.sub_eq_mul_neg ensuring that the types unfold better.

theorem division_def {G : Type u_1} [div_inv_monoid G] (a b : G) :

a / b = a * b⁻¹

Alias of div_eq_mul_inv.

@[instance]

def subtraction_monoid.to_has_involutive_neg (G : Type u) [self : subtraction_monoid G] :

has_involutive_neg G

@[instance]

def subtraction_monoid.to_sub_neg_monoid (G : Type u) [self : subtraction_monoid G] :

sub_neg_monoid G

@[class]

structure subtraction_monoid (G : Type u) :

Type u

add : G → G → G
add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
zero : G
zero_add : ∀ (a : G), 0 + a = a
add_zero : ∀ (a : G), a + 0 = a
nsmul : ℕ → G → G
nsmul_zero' : (∀ (x : G), subtraction_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : G), subtraction_monoid.nsmul n.succ x = x + subtraction_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"
zsmul : ℤ → G → G
zsmul_zero' : (∀ (a : G), subtraction_monoid.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : G), subtraction_monoid.zsmul (int.of_nat n.succ) a = a + subtraction_monoid.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : G), subtraction_monoid.zsmul -[1+ n] a = -subtraction_monoid.zsmul ↑(n.succ) a) . "try_refl_tac"
neg_neg : ∀ (x : G), --x = x
neg_add_rev : ∀ (a b : G), -(a + b) = -b + -a
neg_eq_of_add : ∀ (a b : G), a + b = 0 → -a = b

A subtraction_monoid is a sub_neg_monoid with involutive negation and such that -(a + b) = -b + -a and a + b = 0 → -a = b.

Instances of this typeclass

Instances of other typeclasses for subtraction_monoid

subtraction_monoid.has_sizeof_inst

@[class]

structure division_monoid (G : Type u) :

Type u

mul : G → G → G
mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one : G
one_mul : ∀ (a : G), 1 * a = a
mul_one : ∀ (a : G), a * 1 = a
npow : ℕ → G → G
npow_zero' : (∀ (x : G), division_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : G), division_monoid.npow n.succ x = x * division_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"
zpow : ℤ → G → G
zpow_zero' : (∀ (a : G), division_monoid.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : G), division_monoid.zpow (int.of_nat n.succ) a = a * division_monoid.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : G), division_monoid.zpow -[1+ n] a = (division_monoid.zpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
inv_inv : ∀ (x : G), x⁻¹ ⁻¹ = x
mul_inv_rev : ∀ (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
inv_eq_of_mul : ∀ (a b : G), a * b = 1 → a⁻¹ = b

A division_monoid is a div_inv_monoid with involutive inversion and such that (a * b)⁻¹ = b⁻¹ * a⁻¹ and a * b = 1 → a⁻¹ = b.

This is the immediate common ancestor of group and group_with_zero.

Instances of this typeclass

Instances of other typeclasses for division_monoid

division_monoid.has_sizeof_inst

@[instance]

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

div_inv_monoid G

@[instance]

def division_monoid.to_has_involutive_inv (G : Type u) [self : division_monoid G] :

has_involutive_inv G

@[simp]

theorem mul_inv_rev {G : Type u_1} [division_monoid G] (a b : G) :

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

@[simp]

theorem neg_add_rev {G : Type u_1} [subtraction_monoid G] (a b : G) :

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

theorem neg_eq_of_add_eq_zero_right {G : Type u_1} [subtraction_monoid G] {a b : G} :

a + b = 0 → -a = b

theorem inv_eq_of_mul_eq_one_right {G : Type u_1} [division_monoid G] {a b : G} :

a * b = 1 → a⁻¹ = b

@[instance]

def subtraction_comm_monoid.to_subtraction_monoid (G : Type u) [self : subtraction_comm_monoid G] :

subtraction_monoid G

@[instance]

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

add_comm_monoid G

@[class]

structure subtraction_comm_monoid (G : Type u) :

Type u

add : G → G → G
add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
zero : G
zero_add : ∀ (a : G), 0 + a = a
add_zero : ∀ (a : G), a + 0 = a
nsmul : ℕ → G → G
nsmul_zero' : (∀ (x : G), subtraction_comm_monoid.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : G), subtraction_comm_monoid.nsmul n.succ x = x + subtraction_comm_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"
zsmul : ℤ → G → G
zsmul_zero' : (∀ (a : G), subtraction_comm_monoid.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : G), subtraction_comm_monoid.zsmul (int.of_nat n.succ) a = a + subtraction_comm_monoid.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : G), subtraction_comm_monoid.zsmul -[1+ n] a = -subtraction_comm_monoid.zsmul ↑(n.succ) a) . "try_refl_tac"
neg_neg : ∀ (x : G), --x = x
neg_add_rev : ∀ (a b : G), -(a + b) = -b + -a
neg_eq_of_add : ∀ (a b : G), a + b = 0 → -a = b
add_comm : ∀ (a b : G), a + b = b + a

Commutative subtraction_monoid.

Instances of this typeclass

Instances of other typeclasses for subtraction_comm_monoid

subtraction_comm_monoid.has_sizeof_inst

@[instance]

def division_comm_monoid.to_comm_monoid (G : Type u) [self : division_comm_monoid G] :

@[class]

structure division_comm_monoid (G : Type u) :

Type u

mul : G → G → G
mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one : G
one_mul : ∀ (a : G), 1 * a = a
mul_one : ∀ (a : G), a * 1 = a
npow : ℕ → G → G
npow_zero' : (∀ (x : G), division_comm_monoid.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : G), division_comm_monoid.npow n.succ x = x * division_comm_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"
zpow : ℤ → G → G
zpow_zero' : (∀ (a : G), division_comm_monoid.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : G), division_comm_monoid.zpow (int.of_nat n.succ) a = a * division_comm_monoid.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : G), division_comm_monoid.zpow -[1+ n] a = (division_comm_monoid.zpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
inv_inv : ∀ (x : G), x⁻¹ ⁻¹ = x
mul_inv_rev : ∀ (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
inv_eq_of_mul : ∀ (a b : G), a * b = 1 → a⁻¹ = b
mul_comm : ∀ (a b : G), a * b = b * a

Commutative division_monoid.

This is the immediate common ancestor of comm_group and comm_group_with_zero.

Instances of this typeclass

Instances of other typeclasses for division_comm_monoid

division_comm_monoid.has_sizeof_inst

@[instance]

def division_comm_monoid.to_division_monoid (G : Type u) [self : division_comm_monoid G] :

division_monoid G

@[class]

structure group (G : Type u) :

Type u

mul : G → G → G
mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
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"
zpow : ℤ → G → G
zpow_zero' : (∀ (a : G), group.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : G), group.zpow (int.of_nat n.succ) a = a * group.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : G), group.zpow -[1+ n] a = (group.zpow ↑(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 of this typeclass

Instances of other typeclasses for group

group.has_sizeof_inst

@[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 : A), a + b + c = a + (b + c)
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"
zsmul : ℤ → A → A
zsmul_zero' : (∀ (a : A), add_group.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : A), add_group.zsmul (int.of_nat n.succ) a = a + add_group.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : A), add_group.zsmul -[1+ n] a = -add_group.zsmul ↑(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 of this typeclass

Instances of other typeclasses for add_group

add_group.has_sizeof_inst

@[instance]

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

sub_neg_monoid A

@[reducible]

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

Equations

add_group.to_add_monoid G = sub_neg_monoid.to_add_monoid G

@[reducible]

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 _ _). See note [reducible non-instances].

Equations

group.to_monoid G = div_inv_monoid.to_monoid G

@[simp]

theorem add_left_neg {G : Type u_1} [add_group G] (a : G) :

-a + a = 0

@[simp]

theorem mul_left_inv {G : Type u_1} [group G] (a : G) :

a⁻¹ * a = 1

theorem neg_add_self {G : Type u_1} [add_group G] (a : G) :

-a + a = 0

theorem inv_mul_self {G : Type u_1} [group G] (a : G) :

a⁻¹ * a = 1

@[simp]

theorem mul_right_inv {G : Type u_1} [group G] (a : G) :

a * a⁻¹ = 1

@[simp]

theorem add_right_neg {G : Type u_1} [add_group G] (a : G) :

a + -a = 0

theorem add_neg_self {G : Type u_1} [add_group G] (a : G) :

a + -a = 0

theorem mul_inv_self {G : Type u_1} [group G] (a : G) :

a * a⁻¹ = 1

@[simp]

theorem inv_mul_cancel_left {G : Type u_1} [group G] (a b : G) :

a⁻¹ * (a * b) = b

@[simp]

theorem neg_add_cancel_left {G : Type u_1} [add_group G] (a b : G) :

-a + (a + b) = b

@[simp]

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

a * (a⁻¹ * b) = b

@[simp]

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

a + (-a + b) = b

@[simp]

theorem add_neg_cancel_right {G : Type u_1} [add_group G] (a b : G) :

a + b + -b = a

@[simp]

theorem mul_inv_cancel_right {G : Type u_1} [group G] (a b : G) :

a * b * b⁻¹ = a

@[simp]

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

a + -b + b = a

@[simp]

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

a * b⁻¹ * b = a

@[protected, instance]

def group.to_division_monoid {G : Type u_1} [group G] :

division_monoid G

Equations

group.to_division_monoid = {mul := group.mul _inst_1, mul_assoc := _, one := group.one _inst_1, one_mul := _, mul_one := _, npow := group.npow _inst_1, npow_zero' := _, npow_succ' := _, inv := group.inv _inst_1, div := group.div _inst_1, div_eq_mul_inv := _, zpow := group.zpow _inst_1, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _}

@[protected, instance]

def add_group.to_division_add_monoid {G : Type u_1} [add_group G] :

subtraction_monoid G

Equations

add_group.to_division_add_monoid = {add := add_group.add _inst_1, add_assoc := _, zero := add_group.zero _inst_1, zero_add := _, add_zero := _, nsmul := add_group.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg _inst_1, sub := add_group.sub _inst_1, sub_eq_add_neg := _, zsmul := add_group.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _}

@[protected, instance]

def group.to_cancel_monoid {G : Type u_1} [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 := _}

@[protected, instance]

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

add_cancel_monoid G

Equations

add_group.to_cancel_add_monoid = {add := add_group.add _inst_1, add_assoc := _, add_left_cancel := _, zero := add_group.zero _inst_1, zero_add := _, add_zero := _, nsmul := add_group.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_right_cancel := _}

theorem group.to_div_inv_monoid_injective {G : Type u_1} :

function.injective (group.to_div_inv_monoid G)

theorem add_group.to_sub_neg_add_monoid_injective {G : Type u_1} :

function.injective (add_group.to_sub_neg_monoid G)

@[instance]

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

Instances for comm_group.to_group

CommGroup.comm_group.to_group.category_theory.bundled_hom.parent_projection

@[class]

structure comm_group (G : Type u) :

Type u

mul : G → G → G
mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
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"
zpow : ℤ → G → G
zpow_zero' : (∀ (a : G), comm_group.zpow 0 a = 1) . "try_refl_tac"
zpow_succ' : (∀ (n : ℕ) (a : G), comm_group.zpow (int.of_nat n.succ) a = a * comm_group.zpow (int.of_nat n) a) . "try_refl_tac"
zpow_neg' : (∀ (n : ℕ) (a : G), comm_group.zpow -[1+ n] a = (comm_group.zpow ↑(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 of this typeclass

Instances of other typeclasses for comm_group

comm_group.has_sizeof_inst

@[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 : G), a + b + c = a + (b + c)
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"
zsmul : ℤ → G → G
zsmul_zero' : (∀ (a : G), add_comm_group.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : G), add_comm_group.zsmul (int.of_nat n.succ) a = a + add_comm_group.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : G), add_comm_group.zsmul -[1+ n] a = -add_comm_group.zsmul ↑(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 of this typeclass

Instances of other typeclasses for add_comm_group

add_comm_group.has_sizeof_inst

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

Instances for add_comm_group.to_add_group

AddCommGroup.comm_group.to_group.category_theory.bundled_hom.parent_projection

theorem add_comm_group.to_add_group_injective {G : Type u} :

function.injective (add_comm_group.to_add_group G)

theorem comm_group.to_group_injective {G : Type u} :

function.injective (comm_group.to_group G)

@[protected, instance]

def comm_group.to_cancel_comm_monoid {G : Type u_1} [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 := _}

@[protected, instance]

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

add_cancel_comm_monoid G

Equations

add_comm_group.to_cancel_add_comm_monoid = {add := add_comm_group.add _inst_1, add_assoc := _, add_left_cancel := _, zero := add_comm_group.zero _inst_1, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

@[protected, instance]

def add_comm_group.to_division_add_comm_monoid {G : Type u_1} [add_comm_group G] :

subtraction_comm_monoid G

Equations

add_comm_group.to_division_add_comm_monoid = {add := add_comm_group.add _inst_1, add_assoc := _, zero := add_comm_group.zero _inst_1, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg _inst_1, sub := add_comm_group.sub _inst_1, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _, add_comm := _}

@[protected, instance]

def comm_group.to_division_comm_monoid {G : Type u_1} [comm_group G] :

division_comm_monoid G

Equations

comm_group.to_division_comm_monoid = {mul := comm_group.mul _inst_1, mul_assoc := _, one := comm_group.one _inst_1, one_mul := _, mul_one := _, npow := comm_group.npow _inst_1, npow_zero' := _, npow_succ' := _, inv := comm_group.inv _inst_1, div := comm_group.div _inst_1, div_eq_mul_inv := _, zpow := comm_group.zpow _inst_1, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _, mul_comm := _}