coe_ofNat_eq_mod — Mathlib

English

Let m > 0 and n ∈ ℕ. Then the natural value of ofNat(n) viewed as an element of Fin(m) equals ofNat(n) modulo m; i.e. the natural value is congruent to n modulo m.

Русский

Пусть m > 0 и n ∈ ℕ. Тогда натуральное значение ofNat(n), рассматриваемое как элемент Fin(m), равно n mod m.

LaTeX

$$$ m > 0 \Rightarrow ((\mathrm{ofNat}(n) : \mathrm{Fin}(m)) : \mathbb{N}) = \mathrm{ofNat}(n) \bmod m $$$

Lean4

@[simp]
theorem coe_ofNat_eq_mod (m n : ℕ) [NeZero m] : ((ofNat(n) : Fin m) : ℕ) = ofNat(n) % m :=
  rfl

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