Commit 2022-03-10 19:33 869ef84f

View on Github →

feat(data/zmod/basic): some lemmas about coercions (#12571) The names here are in line with zmod.nat_coe_zmod_eq_zero_iff_dvd and zmod.int_coe_zmod_eq_zero_iff_dvd a few lines above.

Estimated changes

Modified src/data/zmod/basic.lean

added theorem zmod.int_coe_zmod_eq_iff

added theorem zmod.nat_coe_zmod_eq_iff

added theorem zmod.val_int_cast