Theorem WithTop.coe_neg

Modification history

2024-06-11 07:52
Mathlib/Algebra/Order/Group/WithTop.lean
chore: fix diamond for WithTop subtraction (#13715) …
Deleted WithTop.coe_negView on Github →
2022-12-12 05:26
Mathlib/Algebra/Order/Group/WithTop.lean
feat: port algebra.order.group.with_top (#946) …
Added WithTop.coe_negView on Github →