Commit 2023-12-16 00:58 a45fd777

View on Github →

feat(Data/Fin): add lemmas (#8974)

  • move Nat.dvd_one to Data.Nat.Basic; it should go to Std4;
  • rename Fin.ofNat_eq_val to Fin.ofNat''_eq_cast;
  • add @[simp] lemmas Fin.val_nat_cast, Fin.nat_cast_self, and Fin.nat_cast_eq_zero;
  • add @[simp] to Fin.cast_nat_eq_last and ZMod.val_nat_cast;
  • add binomial_apply_last, as the LHS of binomial_apply_self is no longer in simp normal form.

Estimated changes

modified theorem Fin.cast_nat_eq_last
modified theorem Fin.cast_val_eq_self
added theorem Fin.nat_cast_eq_zero
added theorem Fin.nat_cast_self
added theorem Fin.ofNat''_eq_cast
deleted theorem Fin.ofNat_eq_val
modified theorem Fin.one_eq_zero_iff
modified theorem Fin.val_cast_of_lt
added theorem Fin.val_nat_cast
modified theorem Fin.zero_eq_one_iff
added theorem Nat.dvd_one