Unbundled ordered monoid structures on the order dual.

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯