zero_ne_one'

Mathlib.Data.Fin.SuccPred

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

English

In Fin(n+1) with NeZero n, 0 ≠ 1.

Русский

В Fin(n+1) с NeZero n: 0 ≠ 1.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\ [\\mathrm{NeZero}\\ n] : 0 \\neq 1$$$

Lean4

theorem zero_ne_one' [NeZero n] : (0 : Fin (n + 1)) ≠ 1 :=
  Fin.ne_of_lt one_pos'

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

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

Разделы

Аффилиация

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