mathlib

bc1c4f24 - feat(data/zmod/basic): add simp lemmas about coercions, tidy lemma names (#6280)

feat(data/zmod/basic): add simp lemmas about coercions, tidy lemma names (#6280) Split from #5797. This takes the new proofs without introducing the objectionable names. This also renames a bunch of lemmas from `zmod.cast_*` to `zmod.nat_cast_*` and `zmod.int_cast_*`, in order to distinguish lemmas about `zmod.cast` from lemmas about `nat.cast` and `int.cast` applied with a zmod argument. As an example, `zmod.cast_val` has been renamed to `zmod.nat_cast_zmod_val`, as the lemma statement is defeq to `(nat.cast : ℕ → zmod n) (zmod.val x) = x`, and `zmod.nat_cast_val` is already taken by `nat.cast (zmod.val x) = (x : R)`. The full list of renames: * `zmod.cast_val` → `zmod.nat_cast_zmod_val` * `zmod.cast_self` → `zmod.nat_cast_self` * `zmod.cast_self'` → `zmod.nat_cast_self'` * `zmod.cast_mod_nat` → `zmod.nat_cast_mod` * `zmod.cast_mod_int` → `zmod.int_cast_mod` * `zmod.val_cast_nat` → `zmod.val_nat_cast` * `zmod.coe_to_nat` → `zmod.nat_cast_to_nat` * `zmod.cast_unit_of_coprime` → `coe_unit_of_coprime` * `zmod.cast_nat_abs_val_min_abs` → `zmod.nat_cast_nat_abs_val_min_abs`