Documentation
Mathlib
.
Algebra
.
Ring
.
WithZero
Search
Google site search
return to top
source
Imports
Init
Mathlib.Algebra.GroupWithZero.WithZero
Mathlib.Algebra.Ring.Defs
Imported by
WithZero
.
instLeftDistribClass
WithZero
.
instRightDistribClass
WithZero
.
instDistrib
WithZero
.
instSemiring
Adjoining a zero to a semiring
#
source
instance
WithZero
.
instLeftDistribClass
{α :
Type
u_1}
[
Mul
α
]
[
Add
α
]
[
LeftDistribClass
α
]
:
LeftDistribClass
(
WithZero
α
)
Equations
⋯
=
⋯
source
instance
WithZero
.
instRightDistribClass
{α :
Type
u_1}
[
Mul
α
]
[
Add
α
]
[
RightDistribClass
α
]
:
RightDistribClass
(
WithZero
α
)
Equations
⋯
=
⋯
source
instance
WithZero
.
instDistrib
{α :
Type
u_1}
[
Distrib
α
]
:
Distrib
(
WithZero
α
)
Equations
WithZero.instDistrib
=
Distrib.mk
⋯
⋯
source
instance
WithZero
.
instSemiring
{α :
Type
u_1}
[
Semiring
α
]
:
Semiring
(
WithZero
α
)
Equations
One or more equations did not get rendered due to their size.