Mathlib Map

Structures · Algebra

NonAssocSemiring

A unital but not-necessarily-associative semiring.

Defined in
Mathlib.Algebra.Ring.Defs
Shape
One type argument · adds one_mul, mul_one, natCast_zero, natCast_succ
Open in Mathlib docs

Extends3

Extended by3

Concrete types that are instances34

  • Nat
  • SeparationQuotient
  • Filter.Germ
  • CStarMatrix
  • TensorProduct
  • Unitization
  • WithConv
  • Matrix
  • HahnSeries
  • LocallyConstant
  • DomMulAct
  • QuadraticAlgebra
  • MeasureTheory.SimpleFunc
  • MonoidAlgebra
  • TrivSqZeroExt
  • AddMonoidAlgebra
  • DirectLimit
  • SymAlg
  • DomAddAct
  • SkewMonoidAlgebra
  • PiTensorProduct
  • SetSemiring
  • RingCon.Quotient
  • IncidenceAlgebra
  • Subtype
  • Prod
  • OrderDual
  • ULift
  • MulOpposite
  • Lex
  • AddOpposite
  • ContinuousMap
  • Shrink
  • WithTop

How is a type an instance?

Loading the hierarchy index…

Assumed by925

Ancestors34