Theorem MulOpposite.one_le_op

Modification history

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