Ordered monoid structures on Multiplicative α
and Additive α
. #
Equations
- instLEMultiplicative = inst
Equations
- instLTMultiplicative = 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
- Multiplicative.orderedCommMonoid = let __src := Multiplicative.partialOrder; let __src_1 := Multiplicative.commMonoid; OrderedCommMonoid.mk ⋯
Equations
- Additive.orderedAddCommMonoid = let __src := Additive.partialOrder; let __src_1 := Additive.addCommMonoid; OrderedAddCommMonoid.mk ⋯
Equations
- Multiplicative.orderedCancelAddCommMonoid = let __src := Multiplicative.orderedCommMonoid; OrderedCancelCommMonoid.mk ⋯
Equations
- Additive.orderedCancelAddCommMonoid = let __src := Additive.orderedAddCommMonoid; OrderedCancelAddCommMonoid.mk ⋯
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
- ⋯ = ⋯
Equations
- ⋯ = ⋯
instance
Multiplicative.canonicallyOrderedCommMonoid
{α : Type u_1}
[CanonicallyOrderedAddCommMonoid α]
:
Equations
- Multiplicative.canonicallyOrderedCommMonoid = let __src := Multiplicative.orderedCommMonoid; let __src_1 := Multiplicative.orderBot; let __src_2 := ⋯; CanonicallyOrderedCommMonoid.mk ⋯ ⋯
Equations
- Additive.canonicallyOrderedAddCommMonoid = let __src := Additive.orderedAddCommMonoid; let __src_1 := Additive.orderBot; let __src_2 := ⋯; CanonicallyOrderedAddCommMonoid.mk ⋯ ⋯
instance
Multiplicative.canonicallyLinearOrderedCommMonoid
{α : Type u_1}
[CanonicallyLinearOrderedAddCommMonoid α]
:
Equations
- One or more equations did not get rendered due to their size.
instance
instCanonicallyLinearOrderedAddCommMonoidAdditiveOfCanonicallyLinearOrderedCommMonoid
{α : Type u_1}
[CanonicallyLinearOrderedCommMonoid α]
:
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 α}
: