mathlib3
869ef84f - feat(data/zmod/basic): some lemmas about coercions (#12571)

Commit
4 years ago
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. Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Author
Parents
Loading