Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-16 10:05 500a1d32

View on Github →

feat(data/pnat/find): port over nat.find API (#12413) Didn't port pnat.find_add because I got lost in the proof.

Estimated changes

added theorem pnat.le_one_iff
added theorem pnat.lt_add_left
added theorem pnat.lt_add_right
added theorem pnat.not_lt_one
added theorem pnat.find_comp_succ
added theorem pnat.find_eq_iff
added theorem pnat.find_eq_one
added theorem pnat.find_le
added theorem pnat.find_le_iff
added theorem pnat.find_lt_iff
added theorem pnat.find_mono
added theorem pnat.le_find_iff
added theorem pnat.lt_find_iff
added theorem pnat.one_le_find