English
Modulo in ZNum corresponds to integer modulo after embedding into ℤ.
Русский
Остаток в ZNum соответствует целочисленному остатоку после отображения в ℤ.
LaTeX
$$$\forall n,d:\; ((n % d : ZNum) : \mathbb{Z}) = n % d$$$
Lean4
@[simp, norm_cast]
theorem mod_to_int : ∀ n d, ((n % d : ZNum) : ℤ) = n % d
| 0, _ => (Int.zero_emod _).symm
| pos n, d =>
(Num.cast_toZNum _).trans <|
by
rw [← Num.to_nat_to_int, cast_pos, Num.mod_to_nat, ← PosNum.to_nat_to_int, abs_to_nat]
rfl
| neg n, d =>
(Num.cast_sub' _ _).trans <|
by
rw [← Num.to_nat_to_int, cast_neg, ← Num.to_nat_to_int, Num.succ_to_nat, Num.mod_to_nat, abs_to_nat, ←
Int.subNatNat_eq_coe, n.to_int_eq_succ_pred]
rfl
