coe_intCast — Mathlib

English

Let a be any integer. The integer representative of its residue modulo n equals a modulo n.

Русский

Пусть a – произвольное целое число. Целочисленный представитель остатка a по модулю n равен a mod n.

LaTeX

$$$\forall a \in \mathbb{Z},\ \operatorname{cast}(a \bmod n) = a \bmod n$$$

Lean4

theorem coe_intCast (a : ℤ) : cast (a : ZMod n) = a % n :=
  by
  cases n
  · rw [Int.ofNat_zero, Int.emod_zero, Int.cast_id]; rfl
  · rw [← val_intCast, val]; rfl

Похожие утверждения