Structures · Algebra
IdemSemiring
An idempotent semiring is a semiring with the additional property that addition is idempotent.
- Defined in
- Mathlib.Algebra.Order.Kleene
- Shape
- One type argument · adds add_eq_sup
Extends3
Extended by2
Concrete types that are instances3
- SetSemiring
- Prod
- Submodule
How is a type an instance?
Loading the hierarchy index…
Assumed by22
- add_eq_sup
- add_le_iff
- IdemSemiring.add_eq_sup
- add_eq_right_iff_le
- natCast_eq_one
- add_eq_left_iff_le
- add_idem
- IdemSemiring.toOrderBot
- ofNat_eq_one
- Prod.instIdemSemiring
- IdemSemiring.toSemiring
- Pi.instIdemSemiring
- Function.Injective.idemSemiring
- IdemSemiring.toMulRightMono
- IdemSemiring.toCanonicallyOrderedAdd
- LE.le.add_eq_right
- LE.le.add_eq_left
- IdemSemiring.toSemilatticeSup
- IdemSemiring.toIsOrderedAddMonoid
- IdemSemiring.toMulLeftMono
- add_le
- nsmul_eq_self
Ancestors58
- Add
- AddAction
- AddCommMagma
- AddCommMonoid
- AddCommMonoidWithOne
- AddCommSemigroup
- AddMonoid
- AddMonoidWithOne
- AddSemigroup
- AddSemigroupAction
- AddZero
- AddZeroClass
- Bot
- Distrib
- Dvd
- GradeBoundedOrder
- GradeMaxOrder
- GradeMinOrder
- GradeOrder
- HAdd
- HMul
- HSMul
- HVAdd
- LE
- LT
- Lean.Grind.AddCommMonoid
- Lean.Grind.NatModule
- Lean.Grind.Semiring
- Max
- Monoid
- MonoidWithZero
- Mul
- MulAction
- MulOne
- MulOneClass
- MulZeroClass
- MulZeroOneClass
- NPow
- NSMul
- NatCast
- NonAssocSemiring
- NonUnitalNonAssocSemiring
- NonUnitalSemiring
- Nonempty
- OfNat
- One
- OrderBot
- PartialOrder
- Preorder
- SMul
- Semigroup
- SemigroupAction
- SemigroupWithZero
- SemilatticeSup
- Semiring
- VAdd
- ZSMul
- Zero