ofFin_zero

Mathlib.Data.Fin.Fin2

URI: https://scilib.ai/kg/mathlib#Fin2.ofFin_zero

English

For every n, the image of 0 under Fin2.ofFin is the bottom element of Fin2 n.

Русский

Для любого n образ нуля под отображением Fin2.ofFin совпадает с нижним элементом Fin2 n.

LaTeX

$$$\mathrm{Fin2\text{-}ofFin}(0) = \mathrm{fz}.$$$

Lean4

@[simp]
theorem ofFin_zero (n : Nat) : ofFin 0 = @fz n :=
  rfl

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

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

Разделы

Аффилиация

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