val_natCast — Mathlib

English

Let n > 0 be a natural number and a any natural number. Then the value component of the element a embedded into Fin n equals a mod n; i.e. (a : Fin n).val = a mod n.

Русский

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

LaTeX

$$$\\forall a \\in \\mathbb{N}, \\forall n \\in \\mathbb{N}, 0 < n \\Rightarrow (a : \\mathrm{Fin}(n)).\\mathrm{val} = a \\bmod n$$$

Lean4

@[simp]
theorem val_natCast (a n : ℕ) [NeZero n] : (a : Fin n).val = a % n :=
  rfl

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