one_eq_mk_of_lt

Mathlib.Data.Fin.Basic

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

← MathLib Explorer

English

If n > 1 and h: 1 < n, then 1 = Fin.mk 1 h.

Русский

Если n > 1 и h: 1 < n, то 1 = Fin.mk 1 h.

LaTeX

$$$\\forall {n} (h : 1 < n), 1 = \\mathrm{Fin}.mk 1 h$$$

Lean4

theorem one_eq_mk_of_lt {n : ℕ} (h : 1 < n) :
    have : NeZero n := ⟨Nat.ne_zero_of_lt h⟩
    1 = Fin.mk 1 h :=
  Fin.val_inj.mp (Nat.mod_eq_of_lt h)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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