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.