val_intCast — Mathlib

English

For any a ∈ Int, for NeZero n, ↑(a : ZMod n).val = a % n in the appropriate ring.

Русский

Для любого a ∈ ℤ и не нуля n, оболочка (a : ZMod n).val даёт a mod n.

LaTeX

$$$ \uparrow (a : ZMod n).\mathrm{val} = a \bmod n $$$

Lean4

theorem val_intCast {n : ℕ} (a : ℤ) [NeZero n] : ↑(a : ZMod n).val = a % n :=
  by
  have hle : (0 : ℤ) ≤ ↑(a : ZMod n).val := Int.natCast_nonneg _
  have hlt : ↑(a : ZMod n).val < (n : ℤ) := Int.ofNat_lt.mpr (ZMod.val_lt a)
  refine (Int.emod_eq_of_lt hle hlt).symm.trans ?_
  rw [← ZMod.intCast_eq_intCast_iff', Int.cast_natCast, ZMod.natCast_val, ZMod.cast_id]

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