Structures · Algebra
ExistsMulOfLE
An ordered monoid with one-sided 'division' in the sense that
if a ≤ b, there is some c for which a * c = b. This is a weaker version
of the condition on canonical orderings defined by CanonicallyOrderedMul.
- Shape
- One type argument · adds exists_mul_of_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances3
- Filter.Germ
- Prod
- Multiplicative
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- ExistsMulOfLE.exists_mul_of_le
- exists_one_le_mul_of_le
- le_of_forall_one_lt_le_mul
- Finset.card_Ico_mul_right
- le_of_forall_one_lt_lt_mul'
- exists_pow_lt_of_one_lt
- exists_one_lt_mul_of_lt'
- le_iff_forall_one_lt_le_mul
- Set.Icc_mul_Icc
- Pi.existsMulOfLe
- Prod.instExistsMulOfLE
- le_iff_forall_one_lt_lt_mul'
- lt_iff_exists_one_lt_mul
- Additive.existsAddOfLe
- Set.smul_Icc
- le_iff_exists_one_le_mul
- card_Ico_one_mul
- Filter.Germ.instExistsMulOfLE
Ancestors0
No ancestors.