natCast_eq_last

Mathlib.Data.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.natCast_eq_last

English

The natural embedding of n into Fin (n+1) coincides with the last element: (n : Fin (n+1)) = Fin.last n.

Русский

Естественное приведение числа n к Fin (n+1) совпадает с последним элементом: (n : Fin (n+1)) = Fin.last n.

LaTeX

$$$\\forall n \\in \\mathbb{N}, (n : \\mathrm{Fin}(n+1)) = \\mathrm{Fin}.last\ n$$$

Lean4

@[simp]
theorem natCast_eq_last (n) : (n : Fin (n + 1)) = Fin.last n := by ext; simp

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

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

Разделы

Аффилиация

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