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.

Estimated changes

deleted def Nat.findGreatest
deleted theorem Nat.findGreatest_eq
deleted theorem Nat.findGreatest_eq_iff
deleted theorem Nat.findGreatest_le
deleted theorem Nat.findGreatest_mono
deleted theorem Nat.findGreatest_of_not
deleted theorem Nat.findGreatest_pos
deleted theorem Nat.findGreatest_spec
deleted theorem Nat.findGreatest_succ
deleted theorem Nat.findGreatest_zero
deleted theorem Nat.find_add
deleted theorem Nat.find_comp_succ
deleted theorem Nat.find_eq_iff
deleted theorem Nat.find_eq_zero
deleted theorem Nat.find_le
deleted theorem Nat.find_le_iff
deleted theorem Nat.find_lt_iff
deleted theorem Nat.find_mono
deleted theorem Nat.find_pos
deleted theorem Nat.le_findGreatest
deleted theorem Nat.le_find_iff
deleted theorem Nat.lt_find_iff
added def Nat.findGreatest
added theorem Nat.findGreatest_eq
added theorem Nat.findGreatest_le
added theorem Nat.findGreatest_mono
added theorem Nat.findGreatest_pos
added theorem Nat.findGreatest_spec
added theorem Nat.findGreatest_succ
added theorem Nat.findGreatest_zero
added theorem Nat.find_add
added theorem Nat.find_comp_succ
added theorem Nat.find_eq_iff
added theorem Nat.find_eq_zero
added theorem Nat.find_le
added theorem Nat.find_le_iff
added theorem Nat.find_lt_iff
added theorem Nat.find_mono
added theorem Nat.find_pos
added theorem Nat.le_findGreatest
added theorem Nat.le_find_iff
added theorem Nat.lt_find_iff