mathlib
2f1b3131
- chore(data/zmod): make `zmod.int_cast_zmod_cast` `@[norm_cast]` (#15753)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
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.
Author
Vierkantor
Parents
1b09efe3
Loading