Documentation

Mathlib.Algebra.Order.Group.Opposite

Order instances for MulOpposite/AddOpposite #

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

source
@[instance_reducible]
instance MulOpposite.instPreorder {α : Type u_1} [Preorder α] :
Preorder αᵐᵒᵖ
Equations
source
@[instance_reducible]
instance AddOpposite.instPreorder {α : Type u_1} [Preorder α] :
Preorder αᵃᵒᵖ
Equations
source
@[simp]
theorem MulOpposite.unop_le_unop {α : Type u_1} [Preorder α] {a b : αᵐᵒᵖ} :
unop a ≤ unop b ↔ a ≤ b
source
@[simp]
theorem AddOpposite.unop_le_unop {α : Type u_1} [Preorder α] {a b : αᵃᵒᵖ} :
unop a ≤ unop b ↔ a ≤ b
source
@[simp]
theorem MulOpposite.op_le_op {α : Type u_1} [Preorder α] {a b : α} :
op a ≤ op b ↔ a ≤ b
source
@[simp]
theorem AddOpposite.op_le_op {α : Type u_1} [Preorder α] {a b : α} :
op a ≤ op b ↔ a ≤ b
source
@[instance_reducible]
instance MulOpposite.instPartialOrder {α : Type u_1} [PartialOrder α] :
PartialOrder αᵐᵒᵖ
Equations
source
@[instance_reducible]
instance AddOpposite.instPartialOrder {α : Type u_1} [PartialOrder α] :
PartialOrder αᵃᵒᵖ
Equations
source
instance MulOpposite.instIsOrderedMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] :
IsOrderedMonoid αᵐᵒᵖ
source
instance AddOpposite.instIsOrderedAddMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
IsOrderedAddMonoid αᵃᵒᵖ
source
@[simp]
theorem MulOpposite.unop_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} :
unop a ≤ 1 ↔ a ≤ 1
source
@[simp]
theorem AddOpposite.unop_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} :
unop a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem MulOpposite.one_le_unop {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} :
1 ≤ unop a ↔ 1 ≤ a
source
@[simp]
theorem AddOpposite.nonneg_unop {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} :
0 ≤ unop a ↔ 0 ≤ a
source
@[simp]
theorem MulOpposite.op_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} :
op a ≤ 1 ↔ a ≤ 1
source
@[simp]
theorem AddOpposite.op_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} :
op a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem MulOpposite.one_le_op {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} :
1 ≤ op a ↔ 1 ≤ a
source
@[simp]
theorem AddOpposite.nonneg_op {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} :
0 ≤ op a ↔ 0 ≤ a
source
instance MulOpposite.instIsOrderedAddMonoid {α : Type u_1} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] :
IsOrderedAddMonoid αᵐᵒᵖ
source
@[simp]
theorem MulOpposite.unop_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} :
unop a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem MulOpposite.unop_nonneg {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : αᵐᵒᵖ} :
0 ≤ unop a ↔ 0 ≤ a
source
@[simp]
theorem MulOpposite.op_nonpos {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} :
op a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem MulOpposite.op_nonneg {α : Type u_1} [AddCommMonoid α] [PartialOrder α] {a : α} :
0 ≤ op a ↔ 0 ≤ a
source
instance AddOpposite.instIsOrderedMonoid {α : Type u_1} [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] :
IsOrderedMonoid αᵃᵒᵖ
source
@[simp]
theorem AddOpposite.unop_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} :
unop a ≤ 1 ↔ a ≤ 1
source
@[simp]
theorem AddOpposite.one_le_unop {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : αᵃᵒᵖ} :
1 ≤ unop a ↔ 1 ≤ a
source
@[simp]
theorem AddOpposite.op_le_one {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} :
op a ≤ 1 ↔ a ≤ 1
source
@[simp]
theorem AddOpposite.one_le_op {α : Type u_1} [CommMonoid α] [PartialOrder α] {a : α} :
1 ≤ op a ↔ 1 ≤ a