English
([norm_cast]) The integer cast of a residue, when cast back to ZMod n, yields the same residue: ((cast a : ℤ) : ZMod n) = a.
Русский
([нормальное приведение]) Приведение целого числа к ZMod n, затем возврат обратно даёт тот же класс: ((cast a : ℤ) : ZMod n) = a.
LaTeX
$$$ ((\operatorname{cast} a : \mathbb{Z}) : \mathrm{ZMod} n) = a $$$
Lean4
/-- So-named because the outer coercion is `Int.cast` into `ZMod`. For `Int.cast` into an arbitrary
ring, see `ZMod.intCast_cast`. -/
@[norm_cast]
theorem intCast_zmod_cast (a : ZMod n) : ((cast a : ℤ) : ZMod n) = a :=
by
cases n
· simp [ZMod.cast, ZMod]
· dsimp [ZMod.cast]
rw [Int.cast_natCast, natCast_zmod_val]
