Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-25 10:18 9da47ada

View on Github →

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.

Estimated changes