Bryan Gin-ge Chen (Jan 05 2021 at 21:02):
It seems like it'd be a good idea for us to review all mathematical portions of the Lean 4 standard library and then present suggestions all at once. How much of the algebraic / order hierarchies are in the Lean 4 standard library?
(inspired by Definition of nat multiplication)
Last updated: May 06 2021 at 18:20 UTC