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 #
Typeclass for expressing that a type M₀
with multiplication and a zero satisfies
0 * a = 0
and a * 0 = 0
for all a : M₀
.
- mul : M₀ → M₀ → M₀
- zero : M₀
Zero is a left absorbing element for multiplication
Zero is a right absorbing element for multiplication
Instances
- AddOpposite.instMulZeroClass
- ContinuousMap.instMulZeroClassOfContinuousMul
- DirectLimit.instMulZeroClassOfMulHomClassOfZeroHomClass
- Equiv.instMulZeroClassShrink
- Filter.Germ.instMulZeroClass
- MulOpposite.instMulZeroClass
- Nat.instMulZeroClass
- Pi.mulZeroClass
- Prod.instMulZeroClass
- SeparationQuotient.instMulZeroClass
- ULift.mulZeroClass
- WithBot.instMulZeroClass
- WithTop.instMulZeroClass
- WithZero.mulZeroClass
- instMulZeroClassLex
- instMulZeroClassOrderDual
- instMulZeroClassShrink
A mixin for cancellative multiplication by nonzero elements.
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
- AddMonoidAlgebra.instNoZeroDivisorsOfUniqueSums
- AddOpposite.instNoZeroDivisors
- Associates.instNoZeroDivisors
- CancelMonoidWithZero.to_noZeroDivisors
- Cardinal.noZeroDivisors
- ENNReal.instNoZeroDivisors
- EReal.instNoZeroDivisors
- EuclideanDomain.instNoZeroDivisors
- FreeAlgebra.instNoZeroDivisors
- GroupWithZero.noZeroDivisors
- Ideal.Quotient.noZeroDivisors
- Ideal.instNoZeroDivisors
- IsDomain.to_noZeroDivisors
- LinearOrderedSemiring.noZeroDivisors
- Localization.instNoZeroDivisors
- MonoidAlgebra.instNoZeroDivisorsOfUniqueProds
- MulOpposite.instNoZeroDivisors
- MvPolynomial.instNoZeroDivisors
- NNReal.instNoZeroDivisors
- NonUnitalStarSubalgebra.instNoZeroDivisors
- NonUnitalSubalgebra.noZeroDivisors
- NonUnitalSubsemiringClass.noZeroDivisors
- Nonneg.noZeroDivisors
- NormMulClass.toNoZeroDivisors
- Ordinal.noZeroDivisors
- Polynomial.instNoZeroDivisors
- Set.instNoZeroDivisors
- SetSemiring.instNoZeroDivisors
- Subalgebra.noZeroDivisors
- Subring.instNoZeroDivisorsSubtypeMem
- Subsemiring.noZeroDivisors
- SubsemiringClass.noZeroDivisors
- Subsingleton.to_noZeroDivisors
- WithBot.instNoZeroDivisors
- WithTop.instNoZeroDivisors
- WithZero.noZeroDivisors
- instNoZeroDivisorsLex
- instNoZeroDivisorsOrderDual
A type S₀
is a "semigroup with zero” if it is a semigroup with zero element, and 0
is left
and right absorbing.
Instances
- AddOpposite.instSemigroupWithZero
- ContinuousMap.instSemigroupWithZeroOfContinuousMul
- DirectLimit.instSemigroupWithZeroOfMulHomClassOfZeroHomClass
- Equiv.instSemigroupWithZeroShrink
- MulOpposite.instSemigroupWithZero
- Nat.instSemigroupWithZero
- Pi.semigroupWithZero
- Prod.instSemigroupWithZero
- SeparationQuotient.instSemigroupWithZero
- WithBot.instSemigroupWithZero
- WithTop.instSemigroupWithZero
- WithZero.semigroupWithZero
- instSemigroupWithZeroLex
- instSemigroupWithZeroOrderDual
- instSemigroupWithZeroShrink
A typeclass for non-associative monoids with zero elements.
Instances
- AddOpposite.instMulZeroOneClass
- DirectLimit.instMulZeroOneClass
- EReal.instMulZeroOneClass
- Equiv.instMulZeroOneClassShrink
- Filter.Germ.instMulZeroOneClass
- MulOpposite.instMulZeroOneClass
- Nat.instMulZeroOneClass
- Pi.mulZeroOneClass
- Prod.instMulZeroOneClass
- SeparationQuotient.instMulZeroOneClass
- ULift.mulZeroOneClass
- WithBot.instMulZeroOneClass
- WithTop.instMulZeroOneClass
- WithZero.mulZeroOneClass
- instMulZeroOneClassLex
- instMulZeroOneClassOrderDual
- instMulZeroOneClassShrink
A type M₀
is a “monoid with zero” if it is a monoid with zero element, and 0
is left
and right absorbing.
Instances
- AddOpposite.instMonoidWithZero
- ContinuousLinearMap.monoidWithZero
- ContinuousMap.instMonoidWithZeroOfContinuousMul
- DirectLimit.instMonoidWithZeroOfMonoidWithZeroHomClass
- Filter.Germ.instMonoidWithZero
- FreeAlgebra.instMonoidWithZero
- MulOpposite.instMonoidWithZero
- Nat.instMonoidWithZero
- NonUnitalRingHom.instMonoidWithZero
- NonUnitalStarAlgHom.instMonoidWithZero
- NonUnitalStarRingHom.instMonoidWithZero
- Nonneg.monoidWithZero
- Ordinal.monoidWithZero
- OreLocalization.instMonoidWithZero
- Pi.monoidWithZero
- Prod.instMonoidWithZero
- Real.instMonoidWithZero
- SeparationQuotient.instMonoidWithZero
- Set.Icc.monoidWithZero
- ULift.monoidWithZero
- WithBot.instMonoidWithZero
- WithTop.instMonoidWithZero
- WithZero.monoidWithZero
- instMonoidWithZeroLex
- instMonoidWithZeroOrderDual
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.
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
- Associates.instCommMonoidWithZero
- Cardinal.instCommMonoidWithZero
- CommSemiring.toCommMonoidWithZero
- ContinuousMap.instCommMonoidWithZeroOfContinuousMul
- DirectLimit.instCommMonoidWithZeroOfMonoidWithZeroHomClass
- EReal.instCommMonoidWithZero
- Localization.instCommMonoidWithZero
- Nat.instCommMonoidWithZero
- Nonneg.commMonoidWithZero
- OreLocalization.instCommMonoidWithZero
- Pi.commMonoidWithZero
- Prod.instCommMonoidWithZero
- Real.instCommMonoidWithZero
- SeparationQuotient.instCommMonoidWithZero
- Set.Icc.commMonoidWithZero
- ULift.commMonoidWithZero
- WithBot.instCommMonoidWithZero
- WithTop.instCommMonoidWithZero
- WithZero.commMonoidWithZero
- instCommMonoidWithZeroLex
- instCommMonoidWithZeroOrderDual
- instNNRealCommMonoidWithZero
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
- Associates.instCancelCommMonoidWithZero
- CommGroupWithZero.toCancelCommMonoidWithZero
- FractionalIdeal.cancelCommMonoidWithZero
- Ideal.cancelCommMonoidWithZero
- Int.instCancelCommMonoidWithZero
- IsDomain.toCancelCommMonoidWithZero
- Nat.instCancelCommMonoidWithZero
- PUnit.cancelCommMonoidWithZero
- Set.Icc.cancelCommMonoidWithZero
- instCancelCommMonoidWithZeroLex
- instCancelCommMonoidWithZeroOrderDual
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.
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)⁻¹
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
.
- 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)⁻¹
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
.