succ_zero_eq_one'

Mathlib.Data.Fin.SuccPred

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

English

For any n with NeZero, Fin.succ(0) = 1 in Fin(n+1).

Русский

Для любого n с NeZero: Fin.succ(0) = 1 в Fin(n+1).

LaTeX

$$$\\forall n \\in \\mathbb{N},\\ [\\mathrm{NeZero}\; n]\\;:\\; \\mathrm{Fin}.\\mathrm{succ}(0) = 1$$$

Lean4

@[simp]
theorem succ_zero_eq_one' [NeZero n] : Fin.succ (0 : Fin n) = 1 :=
  by
  cases n
  · exact (NeZero.ne 0 rfl).elim
  · rfl

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

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

Разделы

Аффилиация

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