Mathlib Map

Structures · Algebra

CommSemiring

A commutative semiring is a semiring with commutative multiplication.

Defined in
Mathlib.Algebra.Ring.Defs
Shape
One type argument · adds mul_comm
Open in Mathlib docs

Extends2

Extended by3

Forgetful instances

Every CommSemiring is also a

Provided automatically by

Concrete types that are instances62

  • Int
  • Nat
  • Real
  • Rat
  • Complex
  • SeparationQuotient
  • NNReal
  • CategoryTheory.Functor.obj
  • BitVec
  • ENNReal
  • Polynomial
  • Filter.Germ
  • NNRat
  • TensorProduct
  • Unitization
  • WithConv
  • HahnSeries
  • NonemptyInterval
  • LocallyConstant
  • ENat
  • QuadraticAlgebra
  • MeasureTheory.SimpleFunc
  • MonoidAlgebra
  • TrivSqZeroExt
  • AddMonoidAlgebra
  • DirectLimit
  • DirectSum
  • RestrictScalars
  • Zsqrtd
  • SkewMonoidAlgebra
  • LocalizedModule
  • OreLocalization
  • PiTensorProduct
  • CategoryTheory.Limits.Cone.pt
  • Tropical
  • MvPowerSeries
  • FractionalIdeal
  • ArithmeticFunction
  • Cardinal
  • SymmetricAlgebra
  • RingCon.Quotient
  • Num
  • RingQuot
  • MulActionHom
  • Perfection
  • IsIdempotentElem.Corner
  • SemiRingCat.carrier
  • SemimoduleCat.carrier
  • CommSemiRingCat.carrier
  • Subtype
  • Prod
  • OrderDual
  • ULift
  • MulOpposite
  • Lex
  • AddOpposite
  • HasQuotient.Quotient
  • ContinuousMap
  • Shrink
  • WithTop
  • WithAbs
  • WithBot

How is a type an instance?

Loading the hierarchy index…

Assumed by13,482

Ancestors54