maths in Lean 4 standard library

Stream: maths

[Bryan Gin-ge Chen]

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)