Commit 2022-12-12 05:26 d29c2cb9
View on Github →feat: port algebra.order.group.with_top (#946) Tracking mathlib commit: f178c0e25af359f6cbc72a96a243efd3b12423a3
feat: port algebra.order.group.with_top (#946) Tracking mathlib commit: f178c0e25af359f6cbc72a96a243efd3b12423a3