English
For p prime to p>0, equality n.cast z in ZMod p holds iff there exists k with n = z.val + p k.
Русский
Для p>0 равенство n.cast z в ZMod p эквивалентно существованию k such что n = z.val + p k.
LaTeX
$$$\forall p,n,z\ (p>0),\ n^{\uparrow} = z \iff \exists k, n = z.{\tt val} + p k$$$
Lean4
theorem cast_sub_one {R : Type*} [Ring R] {n : ℕ} (k : ZMod n) :
(cast (k - 1 : ZMod n) : R) = (if k = 0 then (n : R) else cast k) - 1 :=
by
split_ifs with hk
· rw [hk, zero_sub, ZMod.cast_neg_one]
· cases n
· dsimp [ZMod, ZMod.cast]
rw [Int.cast_sub, Int.cast_one]
· dsimp [ZMod, ZMod.cast, ZMod.val]
rw [Fin.coe_sub_one, if_neg]
· rw [Nat.cast_sub, Nat.cast_one]
rwa [Fin.ext_iff, Fin.val_zero, ← Ne, ← Nat.one_le_iff_ne_zero] at hk
· exact hk
