Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-01 10:42 2f1b3131

View on Github →

chore(data/zmod): make zmod.int_cast_zmod_cast @[norm_cast] (#15753) I was suprised that norm_cast couldn't do anything with an expression including (((r : zmod 4) : ℤ) : zmod 4), turns out this lemma was missing a norm_cast attribute.

Estimated changes