Commit 2024-11-30 01:55 eb9d9b39

View on Github →

chore: fix names {un}op_non{neg,pos} (#19575)

Estimated changes

modified theorem MulOpposite.op_nonneg
modified theorem MulOpposite.op_nonpos
modified theorem MulOpposite.unop_nonneg
modified theorem MulOpposite.unop_nonpos