natCast_zmod_val — Mathlib

English

For any n, [NeZero n], and a ∈ ZMod n, the natural cast of a.val back to ZMod n equals a.

Русский

Для любого n с не нулём, и a ∈ ZMod n, натуральное приведение a.val обратно в ZMod n равно a.

LaTeX

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

Lean4

/-- So-named because the coercion is `Nat.cast` into `ZMod`. For `Nat.cast` into an arbitrary ring,
see `ZMod.natCast_val`. -/
theorem natCast_zmod_val {n : ℕ} [NeZero n] (a : ZMod n) : (a.val : ZMod n) = a :=
  by
  cases n
  · cases NeZero.ne 0 rfl
  · apply Fin.cast_val_eq_self

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