top_eq_zero

Mathlib.Order.Fin.Basic

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

English

The top equals zero exactly when n = 1: (⊤ : Fin n) = 0 ⇔ n = 1.

Русский

Верхний элемент равен нулю тогда и только тогда, когда n = 1: (⊤ : Fin n) = 0 ⇔ n = 1.

LaTeX

$$$(\top : \mathrm{Fin}(n)) = 0 \;\Longleftrightarrow\; n = 1$$$

Lean4

@[simp]
theorem top_eq_zero {n : ℕ} [NeZero n] : (⊤ : Fin n) = 0 ↔ n = 1 :=
  eq_comm.trans zero_eq_top

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

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

Разделы

Аффилиация

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