elim0_append

Mathlib.Data.Fin.Tuple.Basic

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

English

The lemma append Fin.elim0 v equals v ∘ Fin.cast (Nat.add_zero _).

Русский

Лемма: append Fin.elim0 v = v ∘ Fin.cast (Nat.add_zero _).

LaTeX

$$$\\mathrm{append}\\ \\mathrm{Fin.elim0}\\ v = v \\circ \\mathrm{Fin.cast}(\\mathrm{Nat.add_zero} _).$$$

Lean4

@[simp]
theorem elim0_append (v : Fin n → α) : append Fin.elim0 v = v ∘ Fin.cast (Nat.zero_add _) :=
  append_left_nil _ _ rfl

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

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

Разделы

Аффилиация

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