Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-19 15:47 72eaefff

View on Github →

feat(data/pnat/basic): add lemmas, move equiv.pnat_equiv_nat (#15508)

  • Add lemmas about pnat.nat_pred and nat.succ_pnat.
  • Use derive for pnat.linear_order.
  • Move equiv.pnat_equiv_nat to data/pnat/basic.
  • Use it in order_iso.pnat_iso_nat (renamed from pnat.succ_order_iso, swaped LHS with RHS).
  • Golf some proofs.

Estimated changes

added theorem nat.nat_pred_succ_pnat
modified theorem nat.succ_pnat_inj
added theorem nat.succ_pnat_mono
modified theorem pnat.coe_eq_one_iff
modified theorem pnat.le_one_iff
modified theorem pnat.lt_add_left
modified theorem pnat.lt_add_right
modified def pnat.nat_pred
modified theorem pnat.nat_pred_add_one
modified theorem pnat.nat_pred_eq_pred
added theorem pnat.nat_pred_inj
added theorem pnat.nat_pred_monotone
modified theorem pnat.one_add_nat_pred
deleted def pnat.succ_order_iso