val_one'

Mathlib.Data.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.val_one'

English

The natural value of 1 in Fin(n) equals 1 modulo n: ((1 : Fin n) : ℕ) = 1 mod n.

Русский

Естественное значение единицы в Fin(n) равно 1 по модулю n: (1 : Fin(n))_val = 1 mod n.

LaTeX

$$$$((1:\mathrm{Fin}(n)):\mathbb{N}) = 1 \bmod n.$$$$

Lean4

theorem val_one' (n : ℕ) [NeZero n] : ((1 : Fin n) : ℕ) = 1 % n :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru