Theorem AddOpposite.one_le_unop

Modification history

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