Structures · Algebra
IdemCommSemiring
An idempotent commutative semiring is a commutative semiring with the additional property that addition is idempotent.
- Defined in
- Mathlib.Algebra.Order.Kleene
- Shape
- One type argument · adds add_eq_sup
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- SetSemiring
- AlgebraicGeometry.Scheme.IdealSheafData
- Prod
- Submodule
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by8
Ancestors68
- Add
- AddAction
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddMonoid
- AddMonoidWithOne
- AddSemigroup
- AddSemigroupAction
- AddZero
- AddZeroClass
- Bot
- CommMagma
- CommMonoid
- CommMonoidWithZero
- CommSemigroup
- CommSemiring
- Distrib
- Dvd
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- HAdd
- HMul
- HSMul
- HVAdd
- IdemSemiring
- LE
- LT
- Lean.Grind.AddCommMonoid
- Lean.Grind.CommSemiring
- Lean.Grind.NatModule
- Lean.Grind.Semiring
- Max
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NPow
- NSMul
- NatCast
- NonAssocCommSemiring
- NonAssocSemiring
- NonUnitalCommSemiring
- NonUnitalNonAssocCommSemiring
- NonUnitalNonAssocSemiring
- NonUnitalSemiring
- Nonempty
- OfNat
- One
- OrderBot
- PartialOrder
- Preorder
- SMul
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SemilatticeSup
- Semiring
- VAdd
- ZSMul
- Zero