Documentation

Mathlib.Algebra.Order.Group.Opposite

Order instances for MulOpposite/AddOpposite #

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

Equations
Equations
@[simp]
theorem AddOpposite.op_le_op {α : Type u_1} [Preorder α] {a : α} {b : α} :
@[simp]
theorem MulOpposite.op_le_op {α : Type u_1} [Preorder α] {a : α} {b : α} :
Equations
Equations
Equations
Equations
@[simp]
@[simp]
@[simp]
theorem AddOpposite.op_nonpos {α : Type u_1} [OrderedAddCommMonoid α] {a : α} :
@[simp]
theorem MulOpposite.op_le_one {α : Type u_1} [OrderedCommMonoid α] {a : α} :
@[simp]
theorem AddOpposite.nonneg_op {α : Type u_1} [OrderedAddCommMonoid α] {a : α} :
@[simp]
theorem MulOpposite.one_le_op {α : Type u_1} [OrderedCommMonoid α] {a : α} :
Equations
Equations
Equations
@[simp]
theorem MulOpposite.op_nonneg {α : Type u_1} [OrderedAddCommMonoid α] {a : α} :
@[simp]
theorem MulOpposite.op_nonpos {α : Type u_1} [OrderedAddCommMonoid α] {a : α} :
Equations
Equations
@[simp]
@[simp]
@[simp]
theorem AddOpposite.op_le_one {α : Type u_1} [OrderedCommMonoid α] {a : α} :
@[simp]
theorem AddOpposite.one_le_op {α : Type u_1} [OrderedCommMonoid α] {a : α} :
Equations