Ordered monoid structures on Multiplicative α
and Additive α
. #
instance
instCanonicallyLinearOrderedAddMonoidAdditive
{α : Type u_1}
[CanonicallyLinearOrderedMonoid α]
:
@[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 α}
: