Ordered monoid structures on Multiplicative α
and Additive α
. #
Equations
- instForAllLEMultiplicative = inst
Equations
- instForAllLTMultiplicative = inst
Equations
- Multiplicative.preorder = inst
Equations
- Multiplicative.partialOrder = inst
Equations
- Additive.partialOrder = inst
Equations
- Multiplicative.linearOrder = inst
Equations
- Additive.linearOrder = inst
Equations
- Multiplicative.orderBot = inst
Equations
- Multiplicative.orderTop = inst
Equations
- Multiplicative.boundedOrder = inst
Equations
- Additive.boundedOrder = inst
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
instance
Multiplicative.canonicallyLinearOrderedMonoid
{α : Type u_1}
[CanonicallyLinearOrderedAddMonoid α]
:
Equations
- One or more equations did not get rendered due to their size.
instance
instCanonicallyLinearOrderedAddMonoidAdditive
{α : Type u_1}
[CanonicallyLinearOrderedMonoid α]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Multiplicative.toAdd_le
{α : Type u_1}
[Preorder α]
{a : Multiplicative α}
{b : Multiplicative α}
:
@[simp]
theorem
Multiplicative.toAdd_lt
{α : Type u_1}
[Preorder α]
{a : Multiplicative α}
{b : Multiplicative α}
: