Commit 2021-02-17 23:53 bc1c4f24

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