Theorem MulOpposite.one_le_unop

Modification history

2024-10-04 04:46

Mathlib/Algebra/Order/Group/Opposite.lean

feat: Order instances for `MulOpposite`/`AddOpposite` (#17201) …

Added MulOpposite.one_le_unop View on Github →