coe_natCast_eq_mod — Mathlib

English

Let m > 0 and n ∈ ℕ. Then the natural value of n viewed as an element of Fin(m) equals n modulo m; i.e. the natural projection of n into Fin(m) followed by the natural inclusion back to ℕ is n mod m.

Русский

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

LaTeX

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

Lean4

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

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