Typeclasses for groups with an adjoined zero element #
This file provides just the typeclass definitions, and the projection lemmas that expose their members.
Main definitions #
Zero is a left absorbing element for multiplication
Zero is a right absorbing element for multiplication
Typeclass for expressing that a type M₀
with multiplication and a zero satisfies
0 * a = 0
and a * 0 = 0
for all a : M₀
.
Instances
A mixin for cancellative multiplication by nonzero elements.
Instances
For all
a
andb
ofG₀
,a * b = 0
impliesa = 0
orb = 0
.
Predicate typeclass for expressing that a * b = 0
implies a = 0
or b = 0
for all a
and b
of type G₀
.
Instances
Zero is a left absorbing element for multiplication
Zero is a right absorbing element for multiplication
A type S₀
is a "semigroup with zero” if it is a semigroup with zero element, and 0
is left
and right absorbing.
Instances
Zero is a left absorbing element for multiplication
Zero is a right absorbing element for multiplication
A typeclass for non-associative monoids with zero elements.
Instances
Zero is a left absorbing element for multiplication
Zero is a right absorbing element for multiplication
A type M₀
is a “monoid with zero” if it is a monoid with zero element, and 0
is left
and right absorbing.
Instances
A type M
is a CancelMonoidWithZero
if it is a monoid with zero element, 0
is left
and right absorbing, and left/right multiplication by a non-zero element is injective.
Instances
Zero is a left absorbing element for multiplication
Zero is a right absorbing element for multiplication
A type M
is a commutative “monoid with zero” if it is a commutative monoid with zero
element, and 0
is left and right absorbing.
Instances
A type M
is a CancelCommMonoidWithZero
if it is a commutative monoid with zero element,
0
is left and right absorbing,
and left/right multiplication by a non-zero element is injective.
Instances
Equations
- CancelCommMonoidWithZero.toCancelMonoidWithZero = let src := (_ : IsCancelMulZero M₀); CancelMonoidWithZero.mk
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹⁻¹ * ··· a⁻¹⁻¹
(n
times)zpow : ℤ → G₀ → G₀a ^ 0 = 1
a ^ (n + 1) = a * a ^ n
a ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹
- toNontrivial : Nontrivial G₀
The inverse of
0
in a group with zero is0
.Every nonzero element of a group with zero is invertible.
A type G₀
is a “group with zero” if it is a monoid with zero element (distinct from 1
)
such that every nonzero element is invertible.
The type is required to come with an “inverse” function, and the inverse of 0
must be 0
.
Examples include division rings and the ordered monoids that are the target of valuations in general valuation theory.
Instances
The power operation:
a ^ n = a * ··· * a
;a ^ (-n) = a⁻¹ * ··· a⁻¹⁻¹ * ··· a⁻¹⁻¹
(n
times)zpow : ℤ → G₀ → G₀a ^ 0 = 1
a ^ (n + 1) = a * a ^ n
a ^ -(n + 1) = (a ^ (n + 1))⁻¹⁻¹
- toNontrivial : Nontrivial G₀
The inverse of
0
in a group with zero is0
.Every nonzero element of a group with zero is invertible.
A type G₀
is a commutative “group with zero”
if it is a commutative monoid with zero element (distinct from 1
)
such that every nonzero element is invertible.
The type is required to come with an “inverse” function, and the inverse of 0
must be 0
.
Instances
In a nontrivial monoid with zero, zero and one are different.
Equations
Pullback a nontrivial
instance along a function sending 0
to 0
and 1
to 1
.
If α
has no zero divisors, then the product of two elements equals zero iff one of them
equals zero.
If α
has no zero divisors, then the product of two elements equals zero iff one of them
equals zero.
If α
has no zero divisors, then the product of two elements is nonzero iff both of them
are nonzero.
If α
has no zero divisors, then for elements a, b : α
, a * b
equals zero iff so is
b * a
.
If α
has no zero divisors, then for elements a, b : α
, a * b
is nonzero iff so is
b * a
.