Structures · Algebra

Semiring

A Semiring is a type with addition, multiplication, a 0 and a 1 where addition is commutative and associative, multiplication is associative and left and right distributive over addition, and 0 and 1 are additive and multiplicative identities.

Defined in: Mathlib.Algebra.Ring.Defs
Shape: One type argument · adds zero_mul, mul_zero, left_distrib, right_distrib, natCast_zero, natCast_succ

Open in Mathlib docs

Extends4

Extended by4

Forgetful instances

Every Semiring is also a

Concrete types that are instances68

Int
Nat
Real
Rat
Complex
SeparationQuotient
NNReal
CategoryTheory.Functor.obj
ContinuousLinearMap
Polynomial
Filter.Germ
BoundedContinuousFunction
CStarMatrix
TensorProduct
Unitization
WithConv
Matrix
HahnSeries
LocallyConstant
DomMulAct
MeasureTheory.SimpleFunc
MonoidAlgebra
TrivSqZeroExt
AddMonoidAlgebra
DirectLimit
DirectSum
RestrictScalars
Zsqrtd
DomAddAct
SkewMonoidAlgebra
ContMDiffMap
LocalizedModule
OreLocalization
PiTensorProduct
CategoryTheory.Limits.Cone.pt
CategoryTheory.End
MvPowerSeries
ArithmeticFunction
Module.End
Representation.IntertwiningMap
Language
RingCon.Quotient
RingQuot
MulActionHom
CentroidHom
IsIdempotentElem.Corner
FreeAlgebra
SemiRingCat.carrier
AddMonoid.End
TensorAlgebra
IncidenceAlgebra
MonCat.carrier
ValuativeRel.WithPreorder
LinearAlgebra.FreeProduct
Subtype
Prod
OrderDual
Set.Elem
ULift
MulOpposite
Lex
AddOpposite
HasQuotient.Quotient
ContinuousMap
Shrink
WithTop
WithAbs
WithZero

How is a type an instance?

Loading the hierarchy index…