Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-15 20:09 1f266d62

View on Github →

feat(data/pnat/basic): succ_nat_pred (#11455)

Estimated changes

added theorem pnat.nat_pred_add_one
added theorem pnat.nat_pred_eq_pred
added theorem pnat.one_add_nat_pred