natCast_toNat — Mathlib

English

For every nonnegative integer z, the natural cast of z to ZMod p equals z viewed as an element of ZMod p; i.e., z.toNat cast to ZMod p equals z.

Русский

Для каждого неотрицательного целого числа z натсовый каст к ZMod p равен z, рассматриваемому как элемент ZMod p; т.е. z.toNat в ZMod p равно z.

LaTeX

$$$\forall z \in \mathbb{Z},\ z \ge 0 \Rightarrow (z.{\rm toNat} : \mathbb{Z}/p\mathbb{Z}) = z$$$

Lean4

@[simp]
theorem natCast_toNat (p : ℕ) : ∀ {z : ℤ} (_h : 0 ≤ z), (z.toNat : ZMod p) = z
  | (n : ℕ), _h => by simp only [Int.cast_natCast, Int.toNat_natCast]
  | Int.negSucc n, h => by simp at h

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