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
instance
Additive.boundedOrder
{α : Type u_1}
[inst : LE α]
[inst : BoundedOrder α]
:
BoundedOrder (Additive α)
Equations
- Additive.boundedOrder = inst
instance
Multiplicative.orderedCancelAddCommMonoid
{α : Type u_1}
[inst : OrderedCancelAddCommMonoid α]
:
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.linearOrderedCommMonoid
{α : Type u_1}
[inst : LinearOrderedAddCommMonoid α]
:
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.existsMulOfLe
{α : Type u_1}
[inst : Add α]
[inst : LE α]
[inst : ExistsAddOfLE α]
:
instance
Additive.existsAddOfLe
{α : Type u_1}
[inst : Mul α]
[inst : LE α]
[inst : ExistsMulOfLE α]
:
instance
Multiplicative.canonicallyOrderedMonoid
{α : Type u_1}
[inst : CanonicallyOrderedAddMonoid α]
:
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}
[inst : CanonicallyLinearOrderedAddMonoid α]
:
Equations
- One or more equations did not get rendered due to their size.
instance
instCanonicallyLinearOrderedAddMonoidAdditive
{α : Type u_1}
[inst : CanonicallyLinearOrderedMonoid α]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Multiplicative.toAdd_le
{α : Type u_1}
[inst : Preorder α]
{a : Multiplicative α}
{b : Multiplicative α}
:
@[simp]
theorem
Multiplicative.toAdd_lt
{α : Type u_1}
[inst : Preorder α]
{a : Multiplicative α}
{b : Multiplicative α}
: