val_natCast — Mathlib

English

For natural numbers n and a, the value of the element a in ZMod n equals a modulo n: (a : ZMod n).val = a mod n.

Русский

Для натуральных чисел n и a значение элемента a в ZMod n равно a по модулю n: (a : ZMod n).val = a mod n.

LaTeX

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

Lean4

@[simp]
theorem val_natCast (n a : ℕ) : (a : ZMod n).val = a % n :=
  by
  cases n
  · rw [Nat.mod_zero]
    exact Int.natAbs_natCast a
  · apply Fin.val_natCast

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