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 SMul
and VAdd
for multiplicative and additive
actions and register the following instances:
Pow M ℕ
, for monoidsM
, andPow G ℤ
for groupsG
;SMul ℕ M
for additive monoidsM
, andSMul ℤ G
for additive groupsG
.
SMul
is typically, but not exclusively, used for scalar multiplication-like operators.
See the module Algebra.AddTorsor
for a motivating example for the name VAdd
(vector addition).
Notation #
+
,-
,*
,/
,^
: the usual arithmetic operations; the underlying functions areAdd.add
,Neg.neg
/Sub.sub
,Mul.mul
,Div.div
, andHPow.hPow
.a • b
is used as notation forHSMul.hSMul a b
.a +ᵥ b
is used as notation forHVAdd.hVAdd a b
.
The notation typeclass for heterogeneous additive actions.
This enables the notation a +ᵥ b : γ
where a : α
, b : β
.
- hVAdd : α → β → γ
a +ᵥ b
computes the sum ofa
andb
. The meaning of this notation is type-dependent.
Instances
The notation typeclass for heterogeneous scalar multiplication.
This enables the notation a • b : γ
where a : α
, b : β
.
It is assumed to represent a left action in some sense.
The notation a • b
is augmented with a macro (below) to have it elaborate as a left action.
Only the b
argument participates in the elaboration algorithm: the algorithm uses the type of b
when calculating the type of the surrounding arithmetic expression
and it tries to insert coercions into b
to get some b'
such that a • b'
has the same type as b'
.
See the module documentation near the macro for more details.
- hSMul : α → β → γ
a • b
computes the product ofa
andb
. The meaning of this notation is type-dependent, but it is intended to be used for left actions.
Instances
a +ᵥ b
computes the sum of a
and b
.
The meaning of this notation is type-dependent.
Equations
- «term_+ᵥ_» = Lean.ParserDescr.trailingNode `«term_+ᵥ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " +ᵥ ") (Lean.ParserDescr.cat `term 66))
Instances For
a -ᵥ b
computes the difference of a
and b
. The meaning of this notation is
type-dependent, but it is intended to be used for additive torsors.
Equations
- «term_-ᵥ_» = Lean.ParserDescr.trailingNode `«term_-ᵥ_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " -ᵥ ") (Lean.ParserDescr.cat `term 66))
Instances For
a • b
computes the product of a
and b
.
The meaning of this notation is type-dependent, but it is intended to be used for left actions.
Equations
- «term_•_» = Lean.ParserDescr.trailingNode `«term_•_» 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " • ") (Lean.ParserDescr.cat `term 73))
Instances For
We have a macro to make x • y
notation participate in the expression tree elaborator,
like other arithmetic expressions such as +
, *
, /
, ^
, =
, inequalities, etc.
The macro is using the leftact%
elaborator introduced in
this RFC.
As a concrete example of the effect of this macro, consider
variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)
#check m + r • n
Without the macro, the expression would elaborate as m + ↑(r • n : ↑N) : M
.
With the macro, the expression elaborates as m + r • (↑n : M) : M
.
To get the first interpretation, one can write m + (r • n :)
.
Here is a quick review of the expression tree elaborator:
- It builds up an expression tree of all the immediately accessible operations
that are marked with
binop%
,unop%
,leftact%
,rightact%
,binrel%
, etc. - It elaborates every leaf term of this tree
(without an expected type, so as if it were temporarily wrapped in
(... :)
). - Using the types of each elaborated leaf, it computes a supremum type they can all be coerced to, if such a supremum exists.
- It inserts coercions around leaf terms wherever needed.
The hypothesis is that individual expression trees tend to be calculations with respect to a single algebraic structure.
Note(kmill): If we were to remove HSMul
and switch to using SMul
directly,
then the expression tree elaborator would not be able to insert coercions within the right operand;
they would likely appear as ↑(x • y)
rather than x • ↑y
, unlike other arithmetic operations.
Invert an element of α.
Equations
- «term_⁻¹» = Lean.ParserDescr.trailingNode `«term_⁻¹» 1024 1024 (Lean.ParserDescr.symbol "⁻¹")
Instances For
A mixin for cancellative multiplication.
- mul_left_cancel : ∀ (a b c : G), a * b = a * c → b = c
- mul_right_cancel : ∀ (a b c : G), a * b = c * b → a = c
Instances
A mixin for cancellative addition.
- add_left_cancel : ∀ (a b c : G), a + b = a + c → b = c
- add_right_cancel : ∀ (a b c : G), a + b = c + b → a = c
Instances
Any CommMagma G
that satisfies IsRightCancelMul G
also satisfies IsLeftCancelMul G
.
Any AddCommMagma G
that satisfies
IsRightCancelAdd G
also satisfies IsLeftCancelAdd G
.
Any CommMagma G
that satisfies IsLeftCancelMul G
also satisfies IsRightCancelMul G
.
Any AddCommMagma G
that satisfies
IsLeftCancelAdd G
also satisfies IsRightCancelAdd G
.
Any CommMagma G
that satisfies IsLeftCancelMul G
also satisfies IsCancelMul G
.
Any AddCommMagma G
that satisfies
IsLeftCancelAdd G
also satisfies IsCancelAdd G
.
Any CommMagma G
that satisfies IsRightCancelMul G
also satisfies IsCancelMul G
.
Any AddCommMagma G
that satisfies
IsRightCancelAdd G
also satisfies IsCancelAdd G
.
Any LeftCancelSemigroup
satisfies IsLeftCancelMul
.
Equations
- ⋯ = ⋯
Any AddLeftCancelSemigroup
satisfies
IsLeftCancelAdd
.
Equations
- ⋯ = ⋯
Any RightCancelSemigroup
satisfies IsRightCancelMul
.
Equations
- ⋯ = ⋯
Any AddRightCancelSemigroup
satisfies
IsRightCancelAdd
.
Equations
- ⋯ = ⋯
Design note on AddMonoid
and Monoid
#
An AddMonoid
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 AddMonoid
(which is by
default equal to the naive action a + ... + a
, but can be adjusted when needed), and declare
a 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 AddMonoid
). In this way, the two natural 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.
Scalar multiplication by repeated self-addition, the additive version of exponentation by repeated squaring.
Equations
- nsmulBinRec k m = nsmulBinRec.go k 0 m
Instances For
Auxiliary tail-recursive implementation for nsmulBinRec
Equations
- nsmulBinRec.go 0 x✝ x = x✝
- nsmulBinRec.go k.succ x✝ x = if k &&& 1 = 1 then nsmulBinRec.go ((k + 1) >>> 1) x✝ (x + x) else nsmulBinRec.go ((k + 1) >>> 1) (x✝ + x) (x + x)
Instances For
Auxiliary tail-recursive implementation for npowBinRec
Equations
- npowBinRec.go 0 x✝ x = x✝
- npowBinRec.go k.succ x✝ x = if k &&& 1 = 1 then npowBinRec.go ((k + 1) >>> 1) x✝ (x * x) else npowBinRec.go ((k + 1) >>> 1) (x✝ * x) (x * x)
Instances For
An abbreviation for npowRec
with an additional typeclass assumption on associativity
so that we can use @[csimp]
to replace it with an implementation by repeated squaring
in compiled code.
Equations
- npowRecAuto k m = npowRec k m
Instances For
An abbreviation for nsmulRec
with an additional typeclass assumptions on associativity
so that we can use @[csimp]
to replace it with an implementation by repeated doubling in compiled
code as an automatic parameter.
Equations
- nsmulRecAuto k m = nsmulRec k m
Instances For
An abbreviation for npowBinRec
with an additional typeclass assumption on associativity
so that we can use it in @[csimp]
for more performant code generation.
Equations
- npowBinRecAuto k m = npowBinRec k m
Instances For
An abbreviation for nsmulBinRec
with an additional typeclass assumption on associativity
so that we can use it in @[csimp]
for more performant code generation
as an automatic parameter.
Equations
- nsmulBinRecAuto k m = nsmulBinRec k m
Instances For
An AddMonoid
is an AddSemigroup
with an element 0
such that 0 + a = a + 0 = a
.
- add : M → M → M
- zero : M
- nsmul : ℕ → M → M
Multiplication by a natural number. Set this to
nsmulRec
unlessModule
diamonds are possible. - nsmul_zero : ∀ (x : M), AddMonoid.nsmul 0 x = 0
Multiplication by
(0 : ℕ)
gives0
. - nsmul_succ : ∀ (n : ℕ) (x : M), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
Multiplication by
(n + 1 : ℕ)
behaves as expected.
Instances
A Monoid
is a Semigroup
with an element 1
such that 1 * a = a * 1 = a
.
- mul : M → M → M
- one : M
- npow : ℕ → M → M
Raising to the power of a natural number.
- npow_zero : ∀ (x : M), Monoid.npow 0 x = 1
Raising to the power
(0 : ℕ)
gives1
. - npow_succ : ∀ (n : ℕ) (x : M), Monoid.npow (n + 1) x = Monoid.npow n x * x
Raising to the power
(n + 1 : ℕ)
behaves as expected.
Instances
Equations
- Monoid.toNatPow = { pow := fun (x : M) (n : ℕ) => Monoid.npow n x }
An additive commutative monoid is an additive monoid with commutative (+)
.
- add : M → M → M
- zero : M
- nsmul_zero : ∀ (x : M), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : M), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
Instances
A commutative monoid is a monoid with commutative (*)
.
- mul : M → M → M
- one : M
- npow_zero : ∀ (x : M), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : M), Monoid.npow (n + 1) x = Monoid.npow n x * x
Instances
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 AddLeftCancelSemigroup
is not enough.
- add : M → M → M
- zero : M
- nsmul_zero : ∀ (x : M), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : M), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- add_left_cancel : ∀ (a b c : M), a + b = a + c → b = c
Instances
A monoid in which multiplication is left-cancellative.
- mul : M → M → M
- one : M
- npow_zero : ∀ (x : M), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : M), Monoid.npow (n + 1) x = Monoid.npow n x * x
- mul_left_cancel : ∀ (a b c : M), a * b = a * c → b = c
Instances
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 AddRightCancelSemigroup
is not enough.
- add : M → M → M
- zero : M
- nsmul_zero : ∀ (x : M), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : M), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- add_right_cancel : ∀ (a b c : M), a + b = c + b → a = c
Instances
A monoid in which multiplication is right-cancellative.
- mul : M → M → M
- one : M
- npow_zero : ∀ (x : M), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : M), Monoid.npow (n + 1) x = Monoid.npow n x * x
- mul_right_cancel : ∀ (a b c : M), a * b = c * b → a = c
Instances
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 AddRightCancelMonoid
is not enough.
- add : M → M → M
- zero : M
- nsmul_zero : ∀ (x : M), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : M), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- add_left_cancel : ∀ (a b c : M), a + b = a + c → b = c
- add_right_cancel : ∀ (a b c : M), a + b = c + b → a = c
Instances
A monoid in which multiplication is cancellative.
- mul : M → M → M
- one : M
- npow_zero : ∀ (x : M), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : M), Monoid.npow (n + 1) x = Monoid.npow n x * x
- mul_left_cancel : ∀ (a b c : M), a * b = a * c → b = c
- mul_right_cancel : ∀ (a b c : M), a * b = c * b → a = c
Instances
Commutative version of AddCancelMonoid
.
- add : M → M → M
- zero : M
- nsmul_zero : ∀ (x : M), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : M), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- add_left_cancel : ∀ (a b c : M), a + b = a + c → b = c
Instances
Commutative version of CancelMonoid
.
- mul : M → M → M
- one : M
- npow_zero : ∀ (x : M), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : M), Monoid.npow (n + 1) x = Monoid.npow n x * x
- mul_left_cancel : ∀ (a b c : M), a * b = a * c → b = c
Instances
Equations
Equations
The fundamental power operation in a group. zpowRec n a = a*a*...*a
n times, for integer n
.
Use instead a ^ n
, which has better definitional behavior.
Instances For
The fundamental scalar multiplication in an additive group. zpowRec n a = a+a+...+a
n
times, for integer n
. Use instead n • a
, which has better definitional behavior.
Equations
Instances For
Design note on DivInvMonoid
/SubNegMonoid
and DivisionMonoid
/SubtractionMonoid
#
Those two pairs of made-up classes fulfill slightly different roles.
DivInvMonoid
/SubNegMonoid
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
,
GroupWithZero
, DivisionRing
, Field
) and for a few structures with a rather weak
pseudo-inverse (Matrix
).
DivisionMonoid
/SubtractionMonoid
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
DivisionMonoid.div_eq_mul_inv
, you can define/
arbitrarily. - Without
DivisionMonoid.inv_inv
, you can considerWithTop Unit
witha⁻¹ = ⊤
for alla
. - Without
DivisionMonoid.mul_inv_rev
, you can considerWithTop α
witha⁻¹ = a
for alla
whereα
non commutative. - Without
DivisionMonoid.inv_eq_of_mul
, you can consider anyCommMonoid
witha⁻¹ = a
for alla
.
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
.
In a class equipped with instances of both Monoid
and Inv
, this definition records what the
default definition for Div
would be: a * b⁻¹
. This is later provided as the default value for
the Div
instance in DivInvMonoid
.
We keep it as a separate definition rather than inlining it in DivInvMonoid
so that the Div
field of individual DivInvMonoid
s constructed using that default value will not be unfolded at
.instance
transparency.
Equations
- DivInvMonoid.div' a b = a * b⁻¹
Instances For
A DivInvMonoid
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, Div (Foo X)
instance but no
∀ X, Inv (Foo X)
, e.g. when Foo X
is a EuclideanDomain
. Suppose we
also have an instance ∀ X [Cromulent X], GroupWithZero (Foo X)
. Then the
(/)
coming from GroupWithZero.div
cannot be definitionally equal to
the (/)
coming from Foo.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.
- mul : G → G → G
- one : G
- npow_zero : ∀ (x : G), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = Monoid.npow n x * x
- inv : G → G
- div : G → G → G
a / b := a * b⁻¹
- zpow : ℤ → G → G
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹
(n
times) - zpow_zero' : ∀ (a : G), DivInvMonoid.zpow 0 a = 1
a ^ 0 = 1
- zpow_succ' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
a ^ (n + 1) = a ^ n * a
- zpow_neg' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
a ^ -(n + 1) = (a ^ (n + 1))⁻¹
Instances
In a class equipped with instances of both AddMonoid
and Neg
, this definition records what
the default definition for Sub
would be: a + -b
. This is later provided as the default value
for the Sub
instance in SubNegMonoid
.
We keep it as a separate definition rather than inlining it in SubNegMonoid
so that the Sub
field of individual SubNegMonoid
s constructed using that default value will not be unfolded at
.instance
transparency.
Equations
- SubNegMonoid.sub' a b = a + -b
Instances For
A SubNegMonoid
is an AddMonoid
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, Sub (Foo X)
instance but no
∀ X, Neg (Foo X)
. Suppose we also have an instance
∀ X [Cromulent X], AddGroup (Foo X)
. Then the (-)
coming from
AddGroup.sub
cannot be definitionally equal to the (-)
coming from
Foo.Sub
.
In the same way, adding a zsmul
field makes it possible to avoid definitional failures
in diamonds. See the definition of AddMonoid
and Note [forgetful inheritance] for more
explanations on this.
- add : G → G → G
- zero : G
- nsmul_zero : ∀ (x : G), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : G), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : G → G
- sub : G → G → G
- zsmul : ℤ → G → G
Multiplication by an integer. Set this to
zsmulRec
unlessModule
diamonds are possible. - zsmul_zero' : ∀ (a : G), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
Instances
Equations
- DivInvMonoid.Pow = { pow := fun (x : M) (n : ℤ) => DivInvMonoid.zpow n x }
Equations
- SubNegMonoid.SMulInt = { smul := SubNegMonoid.zsmul }
A group is called cyclic if it is generated by a single element.
- exists_zsmul_surjective : ∃ (g : G), Function.Surjective fun (x : ℤ) => x • g
Instances
Alias of zpow_natCast
.
Alias of natCast_zsmul
.
Dividing by an element is the same as multiplying by its inverse.
This is a duplicate of DivInvMonoid.div_eq_mul_inv
ensuring that the types unfold better.
Subtracting an element is the same as adding by its negative.
This is a duplicate of SubNegMonoid.sub_eq_mul_neg
ensuring that the types unfold better.
Alias of div_eq_mul_inv
.
Dividing by an element is the same as multiplying by its inverse.
This is a duplicate of DivInvMonoid.div_eq_mul_inv
ensuring that the types unfold better.
A SubNegMonoid
where -0 = 0
.
- add : G → G → G
- zero : G
- nsmul_zero : ∀ (x : G), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : G), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : G → G
- sub : G → G → G
- sub_eq_add_neg : ∀ (a b : G), a - b = a + -b
- zsmul_zero' : ∀ (a : G), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
Instances
A DivInvMonoid
where 1⁻¹ = 1
.
- mul : G → G → G
- one : G
- npow_zero : ∀ (x : G), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = Monoid.npow n x * x
- inv : G → G
- div : G → G → G
- div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹
- zpow_zero' : ∀ (a : G), DivInvMonoid.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
Instances
A SubtractionMonoid
is a SubNegMonoid
with involutive negation and such that
-(a + b) = -b + -a
and a + b = 0 → -a = b
.
- add : G → G → G
- zero : G
- nsmul_zero : ∀ (x : G), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : G), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : G → G
- sub : G → G → G
- sub_eq_add_neg : ∀ (a b : G), a - b = a + -b
- zsmul_zero' : ∀ (a : G), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
Despite the asymmetry of
neg_eq_of_add
, the symmetric version is true thanks to the involutivity of negation.
Instances
A DivisionMonoid
is a DivInvMonoid
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 GroupWithZero
.
- mul : G → G → G
- one : G
- npow_zero : ∀ (x : G), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = Monoid.npow n x * x
- inv : G → G
- div : G → G → G
- div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹
- zpow_zero' : ∀ (a : G), DivInvMonoid.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
Despite the asymmetry of
inv_eq_of_mul
, the symmetric version is true thanks to the involutivity of inversion.
Instances
Commutative SubtractionMonoid
.
- add : G → G → G
- zero : G
- nsmul_zero : ∀ (x : G), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : G), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : G → G
- sub : G → G → G
- sub_eq_add_neg : ∀ (a b : G), a - b = a + -b
- zsmul_zero' : ∀ (a : G), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- neg_eq_of_add : ∀ (a b : G), a + b = 0 → -a = b
Instances
Commutative DivisionMonoid
.
This is the immediate common ancestor of CommGroup
and CommGroupWithZero
.
- mul : G → G → G
- one : G
- npow_zero : ∀ (x : G), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = Monoid.npow n x * x
- inv : G → G
- div : G → G → G
- div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹
- zpow_zero' : ∀ (a : G), DivInvMonoid.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
- inv_eq_of_mul : ∀ (a b : G), a * b = 1 → a⁻¹ = b
Instances
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.
Use Group.ofLeftAxioms
or Group.ofRightAxioms
to define a group structure
on a type with the minimum proof obligations.
- mul : G → G → G
- one : G
- npow_zero : ∀ (x : G), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = Monoid.npow n x * x
- inv : G → G
- div : G → G → G
- div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹
- zpow_zero' : ∀ (a : G), DivInvMonoid.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
Instances
An AddGroup
is an AddMonoid
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.
Use AddGroup.ofLeftAxioms
or AddGroup.ofRightAxioms
to define an
additive group structure on a type with the minimum proof obligations.
- add : A → A → A
- zero : A
- nsmul_zero : ∀ (x : A), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : A), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : A → A
- sub : A → A → A
- sub_eq_add_neg : ∀ (a b : A), a - b = a + -b
- zsmul_zero' : ∀ (a : A), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : A), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : A), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
Instances
Alias of inv_mul_cancel
.
Alias of mul_inv_cancel
.
Alias of neg_add_cancel
.
Alias of add_neg_cancel
.
Alias of inv_mul_cancel
.
Alias of mul_inv_cancel
.
Alias of neg_add_cancel
.
Alias of add_neg_cancel
.
Equations
- Group.toDivisionMonoid = DivisionMonoid.mk ⋯ ⋯ ⋯
Equations
- AddGroup.toSubtractionMonoid = SubtractionMonoid.mk ⋯ ⋯ ⋯
Equations
- Group.toCancelMonoid = CancelMonoid.mk ⋯
Equations
- AddGroup.toAddCancelMonoid = AddCancelMonoid.mk ⋯
An additive commutative group is an additive group with commutative (+)
.
- add : G → G → G
- zero : G
- nsmul_zero : ∀ (x : G), AddMonoid.nsmul 0 x = 0
- nsmul_succ : ∀ (n : ℕ) (x : G), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : G → G
- sub : G → G → G
- sub_eq_add_neg : ∀ (a b : G), a - b = a + -b
- zsmul_zero' : ∀ (a : G), SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
- neg_add_cancel : ∀ (a : G), -a + a = 0
Instances
A commutative group is a group with commutative (*)
.
- mul : G → G → G
- one : G
- npow_zero : ∀ (x : G), Monoid.npow 0 x = 1
- npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = Monoid.npow n x * x
- inv : G → G
- div : G → G → G
- div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹
- zpow_zero' : ∀ (a : G), DivInvMonoid.zpow 0 a = 1
- zpow_succ' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
- zpow_neg' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
- inv_mul_cancel : ∀ (a : G), a⁻¹ * a = 1
Instances
Equations
- CommGroup.toCancelCommMonoid = CancelCommMonoid.mk ⋯
Equations
- AddCommGroup.toAddCancelCommMonoid = AddCancelCommMonoid.mk ⋯
Equations
- CommGroup.toDivisionCommMonoid = DivisionCommMonoid.mk ⋯
Equations
- AddCommGroup.toDivisionAddCommMonoid = SubtractionCommMonoid.mk ⋯
We initialize all projections for @[simps]
here, so that we don't have to do it in later
files.
Note: the lemmas generated for the npow
/zpow
projections will not apply to x ^ y
, since the
argument order of these projections doesn't match the argument order of ^
.
The nsmul
/zsmul
lemmas will be correct.