Theorem MulOpposite.op_le_one

Modification history

2024-10-04 04:46
Mathlib/Algebra/Order/Group/Opposite.lean
feat: Order instances for `MulOpposite`/`AddOpposite` (#17201) …
Added MulOpposite.op_le_oneView on Github →