Unbundled ordered monoid structures on the order dual.

instance OrderDual.contravariantClass_add_le {α : Type u} [LE α] [Add α] [c : ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : ContravariantClass αᵒᵈ αᵒᵈ (fun (x1 x2 : αᵒᵈ) => x1 + x2) fun (x1 x2 : αᵒᵈ) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance OrderDual.contravariantClass_mul_le {α : Type u} [LE α] [Mul α] [c : ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] : ContravariantClass αᵒᵈ αᵒᵈ (fun (x1 x2 : αᵒᵈ) => x1 * x2) fun (x1 x2 : αᵒᵈ) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance OrderDual.covariantClass_add_le {α : Type u} [LE α] [Add α] [c : CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : CovariantClass αᵒᵈ αᵒᵈ (fun (x1 x2 : αᵒᵈ) => x1 + x2) fun (x1 x2 : αᵒᵈ) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance OrderDual.covariantClass_mul_le {α : Type u} [LE α] [Mul α] [c : CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] : CovariantClass αᵒᵈ αᵒᵈ (fun (x1 x2 : αᵒᵈ) => x1 * x2) fun (x1 x2 : αᵒᵈ) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance OrderDual.contravariantClass_swap_add_le {α : Type u} [LE α] [Add α] [c : ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : ContravariantClass αᵒᵈ αᵒᵈ (Function.swap fun (x1 x2 : αᵒᵈ) => x1 + x2) fun (x1 x2 : αᵒᵈ) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance OrderDual.contravariantClass_swap_mul_le {α : Type u} [LE α] [Mul α] [c : ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] : ContravariantClass αᵒᵈ αᵒᵈ (Function.swap fun (x1 x2 : αᵒᵈ) => x1 * x2) fun (x1 x2 : αᵒᵈ) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance OrderDual.covariantClass_swap_add_le {α : Type u} [LE α] [Add α] [c : CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] : CovariantClass αᵒᵈ αᵒᵈ (Function.swap fun (x1 x2 : αᵒᵈ) => x1 + x2) fun (x1 x2 : αᵒᵈ) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance OrderDual.covariantClass_swap_mul_le {α : Type u} [LE α] [Mul α] [c : CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] : CovariantClass αᵒᵈ αᵒᵈ (Function.swap fun (x1 x2 : αᵒᵈ) => x1 * x2) fun (x1 x2 : αᵒᵈ) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance OrderDual.contravariantClass_add_lt {α : Type u} [LT α] [Add α] [c : ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : ContravariantClass αᵒᵈ αᵒᵈ (fun (x1 x2 : αᵒᵈ) => x1 + x2) fun (x1 x2 : αᵒᵈ) => x1 < x2

Equations

• ⋯ = ⋯

instance OrderDual.contravariantClass_mul_lt {α : Type u} [LT α] [Mul α] [c : ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : ContravariantClass αᵒᵈ αᵒᵈ (fun (x1 x2 : αᵒᵈ) => x1 * x2) fun (x1 x2 : αᵒᵈ) => x1 < x2

Equations

• ⋯ = ⋯

instance OrderDual.covariantClass_add_lt {α : Type u} [LT α] [Add α] [c : CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : CovariantClass αᵒᵈ αᵒᵈ (fun (x1 x2 : αᵒᵈ) => x1 + x2) fun (x1 x2 : αᵒᵈ) => x1 < x2

Equations

• ⋯ = ⋯

instance OrderDual.covariantClass_mul_lt {α : Type u} [LT α] [Mul α] [c : CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : CovariantClass αᵒᵈ αᵒᵈ (fun (x1 x2 : αᵒᵈ) => x1 * x2) fun (x1 x2 : αᵒᵈ) => x1 < x2

Equations

• ⋯ = ⋯

instance OrderDual.contravariantClass_swap_add_lt {α : Type u} [LT α] [Add α] [c : ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : ContravariantClass αᵒᵈ αᵒᵈ (Function.swap fun (x1 x2 : αᵒᵈ) => x1 + x2) fun (x1 x2 : αᵒᵈ) => x1 < x2

Equations

• ⋯ = ⋯

instance OrderDual.contravariantClass_swap_mul_lt {α : Type u} [LT α] [Mul α] [c : ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : ContravariantClass αᵒᵈ αᵒᵈ (Function.swap fun (x1 x2 : αᵒᵈ) => x1 * x2) fun (x1 x2 : αᵒᵈ) => x1 < x2

Equations

• ⋯ = ⋯

instance OrderDual.covariantClass_swap_add_lt {α : Type u} [LT α] [Add α] [c : CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] : CovariantClass αᵒᵈ αᵒᵈ (Function.swap fun (x1 x2 : αᵒᵈ) => x1 + x2) fun (x1 x2 : αᵒᵈ) => x1 < x2

Equations

• ⋯ = ⋯

instance OrderDual.covariantClass_swap_mul_lt {α : Type u} [LT α] [Mul α] [c : CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] : CovariantClass αᵒᵈ αᵒᵈ (Function.swap fun (x1 x2 : αᵒᵈ) => x1 * x2) fun (x1 x2 : αᵒᵈ) => x1 < x2

Equations

• ⋯ = ⋯