Structures · Algebra
IsQuantale
A quantale is a semigroup distributing over a complete lattice.
- Defined in
- Mathlib.Algebra.Order.Quantale
- Shape
- One type argument · adds mul_sSup_distrib, sSup_mul_distrib
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- mul_sSup_distrib
- sSup_mul_distrib
- IsQuantale.mul_sSup_distrib
- IsQuantale.sSup_mul_distrib
- Quantale.instMulRightMono
- Quantale.instMulLeftMono
- Quantale.sup_mul_distrib
- Quantale.bot_mul
- Quantale.leftMulResiduation_le_iff_mul_le
- Quantale.iSup_mul_distrib
- Quantale.rightMulResiduation_le_iff_mul_le
- Quantale.mul_sup_distrib
- Quantale.mul_bot
- Quantale.mul_iSup_distrib
Ancestors0
No ancestors.