Order instances for MulOpposite/AddOpposite

This files transfers order instances and ordered monoid/group instances from α to αᵐᵒᵖ and αᵃᵒᵖ.

instance MulOpposite.instPreorder {α : Type u_1} [Preorder α] : Preorder αᵐᵒᵖ

Equations

• MulOpposite.instPreorder = Preorder.lift MulOpposite.unop

instance AddOpposite.instPreorder {α : Type u_1} [Preorder α] : Preorder αᵃᵒᵖ

Equations

• AddOpposite.instPreorder = Preorder.lift AddOpposite.unop

@[simp]

theorem MulOpposite.unop_le_unop {α : Type u_1} [Preorder α] {a : αᵐᵒᵖ} {b : αᵐᵒᵖ} : MulOpposite.unop a ≤ MulOpposite.unop b ↔ a ≤ b

@[simp]

theorem AddOpposite.unop_le_unop {α : Type u_1} [Preorder α] {a : αᵃᵒᵖ} {b : αᵃᵒᵖ} : AddOpposite.unop a ≤ AddOpposite.unop b ↔ a ≤ b

@[simp]

theorem MulOpposite.op_le_op {α : Type u_1} [Preorder α] {a : α} {b : α} : MulOpposite.op a ≤ MulOpposite.op b ↔ a ≤ b

@[simp]

theorem AddOpposite.op_le_op {α : Type u_1} [Preorder α] {a : α} {b : α} : AddOpposite.op a ≤ AddOpposite.op b ↔ a ≤ b

instance MulOpposite.instPartialOrder {α : Type u_1} [PartialOrder α] : PartialOrder αᵐᵒᵖ

Equations

• MulOpposite.instPartialOrder = PartialOrder.lift MulOpposite.unop ⋯

instance AddOpposite.instPartialOrder {α : Type u_1} [PartialOrder α] : PartialOrder αᵃᵒᵖ

Equations

• AddOpposite.instPartialOrder = PartialOrder.lift AddOpposite.unop ⋯

instance MulOpposite.instOrderedCommMonoid {α : Type u_1} [OrderedCommMonoid α] : OrderedCommMonoid αᵐᵒᵖ

Equations

• MulOpposite.instOrderedCommMonoid = OrderedCommMonoid.mk ⋯

instance AddOpposite.instOrderedAddCommMonoid {α : Type u_1} [OrderedAddCommMonoid α] : OrderedAddCommMonoid αᵃᵒᵖ

Equations

• AddOpposite.instOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

@[simp]

theorem MulOpposite.unop_le_one {α : Type u_1} [OrderedCommMonoid α] {a : αᵐᵒᵖ} : MulOpposite.unop a ≤ 1 ↔ a ≤ 1

@[simp]

theorem AddOpposite.unop_nonpos {α : Type u_1} [OrderedAddCommMonoid α] {a : αᵃᵒᵖ} : AddOpposite.unop a ≤ 0 ↔ a ≤ 0

@[simp]

theorem MulOpposite.one_le_unop {α : Type u_1} [OrderedCommMonoid α] {a : αᵐᵒᵖ} : 1 ≤ MulOpposite.unop a ↔ 1 ≤ a

@[simp]

theorem AddOpposite.nonneg_unop {α : Type u_1} [OrderedAddCommMonoid α] {a : αᵃᵒᵖ} : 0 ≤ AddOpposite.unop a ↔ 0 ≤ a

@[simp]

theorem MulOpposite.op_le_one {α : Type u_1} [OrderedCommMonoid α] {a : α} : MulOpposite.op a ≤ 1 ↔ a ≤ 1

@[simp]

theorem AddOpposite.op_nonpos {α : Type u_1} [OrderedAddCommMonoid α] {a : α} : AddOpposite.op a ≤ 0 ↔ a ≤ 0

@[simp]

theorem MulOpposite.one_le_op {α : Type u_1} [OrderedCommMonoid α] {a : α} : 1 ≤ MulOpposite.op a ↔ 1 ≤ a

@[simp]

theorem AddOpposite.nonneg_op {α : Type u_1} [OrderedAddCommMonoid α] {a : α} : 0 ≤ AddOpposite.op a ↔ 0 ≤ a

instance MulOpposite.instOrderedCommGroup {α : Type u_1} [OrderedCommGroup α] : OrderedCommGroup αᵐᵒᵖ

Equations

• MulOpposite.instOrderedCommGroup = OrderedCommGroup.mk ⋯

instance AddOpposite.instOrderedAddCommGroup {α : Type u_1} [OrderedAddCommGroup α] : OrderedAddCommGroup αᵃᵒᵖ

Equations

• AddOpposite.instOrderedAddCommGroup = OrderedAddCommGroup.mk ⋯

instance MulOpposite.instOrderedAddCommMonoid {α : Type u_1} [OrderedAddCommMonoid α] : OrderedAddCommMonoid αᵐᵒᵖ

Equations

• MulOpposite.instOrderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

@[simp]

theorem MulOpposite.unop_nonneg {α : Type u_1} [OrderedAddCommMonoid α] {a : αᵐᵒᵖ} : MulOpposite.unop a ≤ 0 ↔ a ≤ 0

@[simp]

theorem MulOpposite.unop_nonpos {α : Type u_1} [OrderedAddCommMonoid α] {a : αᵐᵒᵖ} : 0 ≤ MulOpposite.unop a ↔ 0 ≤ a

@[simp]

theorem MulOpposite.op_nonneg {α : Type u_1} [OrderedAddCommMonoid α] {a : α} : MulOpposite.op a ≤ 0 ↔ a ≤ 0

@[simp]

theorem MulOpposite.op_nonpos {α : Type u_1} [OrderedAddCommMonoid α] {a : α} : 0 ≤ MulOpposite.op a ↔ 0 ≤ a

instance MulOpposite.instOrderedAddCommGroup {α : Type u_1} [OrderedAddCommGroup α] : OrderedAddCommGroup αᵐᵒᵖ

Equations

• MulOpposite.instOrderedAddCommGroup = OrderedAddCommGroup.mk ⋯

instance AddOpposite.instOrderedCommMonoid {α : Type u_1} [OrderedCommMonoid α] : OrderedCommMonoid αᵃᵒᵖ

Equations

• AddOpposite.instOrderedCommMonoid = OrderedCommMonoid.mk ⋯

@[simp]

theorem AddOpposite.unop_le_one {α : Type u_1} [OrderedCommMonoid α] {a : αᵃᵒᵖ} : AddOpposite.unop a ≤ 1 ↔ a ≤ 1

@[simp]

theorem AddOpposite.one_le_unop {α : Type u_1} [OrderedCommMonoid α] {a : αᵃᵒᵖ} : 1 ≤ AddOpposite.unop a ↔ 1 ≤ a

@[simp]

theorem AddOpposite.op_le_one {α : Type u_1} [OrderedCommMonoid α] {a : α} : AddOpposite.op a ≤ 1 ↔ a ≤ 1

@[simp]

theorem AddOpposite.one_le_op {α : Type u_1} [OrderedCommMonoid α] {a : α} : 1 ≤ AddOpposite.op a ↔ 1 ≤ a

instance AddOpposite.instOrderedCommGroup {α : Type u_1} [OrderedCommGroup α] : OrderedCommGroup αᵃᵒᵖ

Equations

• AddOpposite.instOrderedCommGroup = OrderedCommGroup.mk ⋯