Structures · Algebra
IsBotZeroClass
A typeclass expressing that the 0 of a type is a bottom element. In a partial OrderBot, this
is equivalent to ⊥ = 0.
- Defined in
- Mathlib.Algebra.Order.IsBotOne
- Shape
- One type argument · adds isBot_zero
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances7
- Finsupp
- DFinsupp
- Fin
- Lex
- WithTop
- Colex
- WithZero
How is a type an instance?
Loading the hierarchy index…
Assumed by91
- zero_le
- pos_iff_ne_zero
- nonpos_iff_eq_zero
- NeZero.pos
- eq_zero_or_pos
- LT.lt.ne_zero
- Order.one_le_iff_ne_zero
- bot_eq_zero
- LT.lt.pos
- zero_lt_iff
- pos_of_gt
- pos_of_ne_zero
- ne_zero_of_lt
- Ne.pos
- le_zero_iff
- Order.lt_one_iff
- not_lt_zero
- Order.le_one_iff
- NeZero.of_gt
- add_pos_of_right
- IsBotZeroClass.toOrderBot
- Order.IsSuccLimit.pos
- Set.Ici_zero_eq_univ
- max_zero
- eq_zero_of_nonpos
- isBot_zero
- Finsupp.support_inf
- Right.pos_add_of_right
- Order.le_two_iff
- Left.pos_add_of_left
- zero_max
- Finsupp.support_sup
- DFinsupp.support_inf
- Finset.sup_eq_zero
- DFinsupp.card_Iic
- Finsupp.card_Iic
- IsBotZeroClass.isBot_zero
- Set.Iio_zero_eq_empty
- Order.IsSuccLimit.natCast_lt
- max_eq_zero
- zero_min
- Finsupp.wellFoundedLT'
- DFinsupp.disjoint_iff
- DFinsupp.Colex.isBotZeroClass
- zero_notMem_iff
- Finsupp.Colex.isBotZeroClass
- WithTop.instIsBotZeroClass
- DFinsupp.Lex.orderBot
- min_eq_zero
- not_lt_zero'
Ancestors0
No ancestors.