Commit 2022-12-12 05:26 d29c2cb9

View on Github →

feat: port algebra.order.group.with_top (#946) Tracking mathlib commit: f178c0e25af359f6cbc72a96a243efd3b12423a3

Estimated changes

added theorem WithTop.coe_neg