Commit 2024-10-04 04:46 7e655050

View on Github →

feat: Order instances for MulOpposite/AddOpposite (#17201) Transfer order and ordered monoid/group/semiring/ring instances from α to αᵐᵒᵖ and αᵃᵒᵖ.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Group/Opposite.lean

added theorem AddOpposite.one_le_op

added theorem AddOpposite.one_le_unop

added theorem AddOpposite.op_le_one

added theorem AddOpposite.unop_le_one

added theorem MulOpposite.one_le_op

added theorem MulOpposite.one_le_unop

added theorem MulOpposite.op_le_one

added theorem MulOpposite.op_le_op

added theorem MulOpposite.op_nonneg

added theorem MulOpposite.op_nonpos

added theorem MulOpposite.unop_le_one

added theorem MulOpposite.unop_le_unop

added theorem MulOpposite.unop_nonneg

added theorem MulOpposite.unop_nonpos

Created Mathlib/Algebra/Order/Ring/Opposite.lean