Commit 2024-06-19 09:36 46c501f8

View on Github →

chore(Algebra/Order/Monoid/Defs): remove unused instances (#13466) We do not need them in Lean4.

Estimated changes