Theorem MulOpposite.unop_nonpos

Modification history

2024-11-30 01:55
Mathlib/Algebra/Order/Group/Opposite.lean
chore: fix names `{un}op_non{neg,pos}` (#19575)
Modified MulOpposite.unop_nonposView on Github →
2024-10-04 04:46
Mathlib/Algebra/Order/Group/Opposite.lean
feat: Order instances for `MulOpposite`/`AddOpposite` (#17201) …
Added MulOpposite.unop_nonposView on Github →