Commit 2024-07-16 00:30 8e2586a3
View on Github →chore: move Nat.find/findGreatest into their own file (#11891)
This lightens the very low-level Mathlib/Data/Nat/Defs.lean
and Mathlib/Init/Data/Nat/Lemmas.lean
a bit.
chore: move Nat.find/findGreatest into their own file (#11891)
This lightens the very low-level Mathlib/Data/Nat/Defs.lean
and Mathlib/Init/Data/Nat/Lemmas.lean
a bit.