castLE_rfl

Mathlib.Data.Fin.SuccPred

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

English

For n, Fin.castLE(le_refl n) = id.

Русский

Для n, Fin.castLE(le_refl n) = id.

LaTeX

$$$\\forall n \\in \\mathbb{N},\\; \\mathrm{Fin.castLE}(\\mathrm{le\\_refl}\\; n) = \\mathrm{id}$$$

Lean4

@[simp]
theorem castLE_rfl (n : ℕ) : Fin.castLE (le_refl n) = id :=
  rfl

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

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

Разделы

Аффилиация

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