Ordered monoid structures on Multiplicative α and Additive α.

ink

instance instForAllLEMultiplicative {α : Type u_1} [inst : LE α] : LE (Multiplicative α)

Equations

• instForAllLEMultiplicative = inst

ink

instance instForAllLEAdditive {α : Type u_1} [inst : LE α] : LE (Additive α)

Equations

• instForAllLEAdditive = inst

ink

instance instForAllLTMultiplicative {α : Type u_1} [inst : LT α] : LT (Multiplicative α)

Equations

• instForAllLTMultiplicative = inst

ink

instance instForAllLTAdditive {α : Type u_1} [inst : LT α] : LT (Additive α)

Equations

• instForAllLTAdditive = inst

ink

instance Multiplicative.preorder {α : Type u_1} [inst : Preorder α] : Preorder (Multiplicative α)

Equations

• Multiplicative.preorder = inst

ink

instance Additive.preorder {α : Type u_1} [inst : Preorder α] : Preorder (Additive α)

Equations

• Additive.preorder = inst

ink

instance Multiplicative.partialOrder {α : Type u_1} [inst : PartialOrder α] : PartialOrder (Multiplicative α)

Equations

• Multiplicative.partialOrder = inst

ink

instance Additive.partialOrder {α : Type u_1} [inst : PartialOrder α] : PartialOrder (Additive α)

Equations

• Additive.partialOrder = inst

ink

instance Multiplicative.linearOrder {α : Type u_1} [inst : LinearOrder α] : LinearOrder (Multiplicative α)

Equations

• Multiplicative.linearOrder = inst

ink

instance Additive.linearOrder {α : Type u_1} [inst : LinearOrder α] : LinearOrder (Additive α)

Equations

• Additive.linearOrder = inst

ink

instance Multiplicative.orderBot {α : Type u_1} [inst : LE α] [inst : OrderBot α] : OrderBot (Multiplicative α)

Equations

• Multiplicative.orderBot = inst

ink

instance Additive.orderBot {α : Type u_1} [inst : LE α] [inst : OrderBot α] : OrderBot (Additive α)

Equations

• Additive.orderBot = inst

ink

instance Multiplicative.orderTop {α : Type u_1} [inst : LE α] [inst : OrderTop α] : OrderTop (Multiplicative α)

Equations

• Multiplicative.orderTop = inst

ink

instance Additive.orderTop {α : Type u_1} [inst : LE α] [inst : OrderTop α] : OrderTop (Additive α)

Equations

• Additive.orderTop = inst

ink

instance Multiplicative.boundedOrder {α : Type u_1} [inst : LE α] [inst : BoundedOrder α] : BoundedOrder (Multiplicative α)

Equations

• Multiplicative.boundedOrder = inst

ink

instance Additive.boundedOrder {α : Type u_1} [inst : LE α] [inst : BoundedOrder α] : BoundedOrder (Additive α)

Equations

• Additive.boundedOrder = inst

ink

instance Multiplicative.orderedCommMonoid {α : Type u_1} [inst : OrderedAddCommMonoid α] : OrderedCommMonoid (Multiplicative α)

Equations

• Multiplicative.orderedCommMonoid = let src := Multiplicative.partialOrder; let src_1 := Multiplicative.commMonoid; OrderedCommMonoid.mk (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b)

ink

instance Additive.orderedAddCommMonoid {α : Type u_1} [inst : OrderedCommMonoid α] : OrderedAddCommMonoid (Additive α)

Equations

• Additive.orderedAddCommMonoid = let src := Additive.partialOrder; let src_1 := Additive.addCommMonoid; OrderedAddCommMonoid.mk (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b)

ink

instance Multiplicative.orderedCancelAddCommMonoid {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] : OrderedCancelCommMonoid (Multiplicative α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance Additive.orderedCancelAddCommMonoid {α : Type u_1} [inst : OrderedCancelCommMonoid α] : OrderedCancelAddCommMonoid (Additive α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance Multiplicative.linearOrderedCommMonoid {α : Type u_1} [inst : LinearOrderedAddCommMonoid α] : LinearOrderedCommMonoid (Multiplicative α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance Additive.linearOrderedAddCommMonoid {α : Type u_1} [inst : LinearOrderedCommMonoid α] : LinearOrderedAddCommMonoid (Additive α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance Multiplicative.existsMulOfLe {α : Type u_1} [inst : Add α] [inst : LE α] [inst : ExistsAddOfLE α] : ExistsMulOfLE (Multiplicative α)

Equations

• @Multiplicative.existsMulOfLe = @Multiplicative.existsMulOfLe.proof_1

ink

instance Additive.existsAddOfLe {α : Type u_1} [inst : Mul α] [inst : LE α] [inst : ExistsMulOfLE α] : ExistsAddOfLE (Additive α)

Equations

• @Additive.existsAddOfLe = @Additive.existsAddOfLe.proof_1

ink

instance Multiplicative.canonicallyOrderedMonoid {α : Type u_1} [inst : CanonicallyOrderedAddMonoid α] : CanonicallyOrderedMonoid (Multiplicative α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance Additive.canonicallyOrderedAddMonoid {α : Type u_1} [inst : CanonicallyOrderedMonoid α] : CanonicallyOrderedAddMonoid (Additive α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance Multiplicative.canonicallyLinearOrderedMonoid {α : Type u_1} [inst : CanonicallyLinearOrderedAddMonoid α] : CanonicallyLinearOrderedMonoid (Multiplicative α)

Equations

• One or more equations did not get rendered due to their size.

ink

instance instCanonicallyLinearOrderedAddMonoidAdditive {α : Type u_1} [inst : CanonicallyLinearOrderedMonoid α] : CanonicallyLinearOrderedAddMonoid (Additive α)

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

theorem Additive.ofMul_le {α : Type u_1} [inst : Preorder α] {a : α} {b : α} : ↑Additive.ofMul a ≤ ↑Additive.ofMul b ↔ a ≤ b

ink

@[simp]

theorem Additive.ofMul_lt {α : Type u_1} [inst : Preorder α] {a : α} {b : α} : ↑Additive.ofMul a < ↑Additive.ofMul b ↔ a < b

ink

@[simp]

theorem Additive.toMul_le {α : Type u_1} [inst : Preorder α] {a : Additive α} {b : Additive α} : ↑Additive.toMul a ≤ ↑Additive.toMul b ↔ a ≤ b

ink

@[simp]

theorem Additive.toMul_lt {α : Type u_1} [inst : Preorder α] {a : Additive α} {b : Additive α} : ↑Additive.toMul a < ↑Additive.toMul b ↔ a < b

ink

@[simp]

theorem Multiplicative.ofAdd_le {α : Type u_1} [inst : Preorder α] {a : α} {b : α} : ↑Multiplicative.ofAdd a ≤ ↑Multiplicative.ofAdd b ↔ a ≤ b

ink

@[simp]

theorem Multiplicative.ofAdd_lt {α : Type u_1} [inst : Preorder α] {a : α} {b : α} : ↑Multiplicative.ofAdd a < ↑Multiplicative.ofAdd b ↔ a < b

ink

@[simp]

theorem Multiplicative.toAdd_le {α : Type u_1} [inst : Preorder α] {a : Multiplicative α} {b : Multiplicative α} : ↑Multiplicative.toAdd a ≤ ↑Multiplicative.toAdd b ↔ a ≤ b

ink

@[simp]

theorem Multiplicative.toAdd_lt {α : Type u_1} [inst : Preorder α] {a : Multiplicative α} {b : Multiplicative α} : ↑Multiplicative.toAdd a < ↑Multiplicative.toAdd b ↔ a < b