mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(Algebra/Order/Field/Basic): add Nat cast lemmas

Open mariainesdff opened this issue 4 months ago • 2 comments

These lemmas have one-line proofs, but I use them enough times in #15373 that I think it makes sense to introduce them.

Open in Gitpod

mariainesdff avatar Oct 24 '24 13:10 mariainesdff