Theorem MulOpposite.op_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.op_nonpos View on Github →

2024-10-04 04:46

Mathlib/Algebra/Order/Group/Opposite.lean

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

Added MulOpposite.op_nonpos View on Github →