mathlib3
9da47ada - feat(data/zmod): lemmas about coercions to zmod (#2802)

Commit
5 years ago
feat(data/zmod): lemmas about coercions to zmod (#2802) I'm not particularly happy with the location of these new lemmas within the file `data.zmod`. If anyone has a suggestion that they should be some particular place higher or lower in the file, that would be welcome. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading