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 #
A mixin for cancellative multiplication by nonzero elements.
Instances
Predicate typeclass for expressing that a * b = 0
implies a = 0
or b = 0
for all a
and b
of type G₀
.
For all
a
andb
ofG₀
,a * b = 0
impliesa = 0
orb = 0
.
Instances
A type S₀
is a "semigroup with zero” if it is a semigroup with zero element, and 0
is left
and right absorbing.
Instances
A typeclass for non-associative monoids with zero elements.
Instances
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
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 = CancelMonoidWithZero.mk
Prop-valued mixin for a monoid with zero to be equipped with a cancelling division.
The obvious use case is groups with zero, but this condition is also satisfied by ℕ
, ℤ
and, more
generally, any euclidean domain.
Instances
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.
- mul : G₀ → G₀ → G₀
- one : G₀
- zero : G₀
- inv : G₀ → G₀
- div : G₀ → G₀ → G₀
- zpow_neg' (n : ℕ) (a : G₀) : GroupWithZero.zpow (Int.negSucc n) a = (GroupWithZero.zpow (↑n.succ) a)⁻¹
- exists_pair_ne : ∃ (x : G₀), ∃ (y : G₀), x ≠ y
The inverse of
0
in a group with zero is0
.Every nonzero element of a group with zero is invertible.
Instances
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
.
- mul : G₀ → G₀ → G₀
- one : G₀
- zero : G₀
- inv : G₀ → G₀
- div : G₀ → G₀ → G₀
- zpow_succ' (n : ℕ) (a : G₀) : CommGroupWithZero.zpow (↑n.succ) a = CommGroupWithZero.zpow (↑n) a * a
- zpow_neg' (n : ℕ) (a : G₀) : CommGroupWithZero.zpow (Int.negSucc n) a = (CommGroupWithZero.zpow (↑n.succ) a)⁻¹
- exists_pair_ne : ∃ (x : G₀), ∃ (y : G₀), x ≠ y
Instances
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
.