Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 2f1b313

Browse files
committed
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.
1 parent 1b09efe commit 2f1b313

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/data/zmod/basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ nat_cast_right_inverse.surjective
138138

139139
/-- So-named because the outer coercion is `int.cast` into `zmod`. For `int.cast` into an arbitrary
140140
ring, see `zmod.int_cast_cast`. -/
141-
lemma int_cast_zmod_cast (a : zmod n) : ((a : ℤ) : zmod n) = a :=
141+
@[norm_cast] lemma int_cast_zmod_cast (a : zmod n) : ((a : ℤ) : zmod n) = a :=
142142
begin
143143
cases n,
144144
{ rw [int.cast_id a, int.cast_id a], },

0 commit comments

Comments
 (0)