equivPair_tail — Mathlib

English

The constructor cons is equal to smul by m on the tail when fstIdx and head satisfy the usual nondegeneracy conditions.

Русский

Конструктор cons равен smul на хвосте при выполнении обычных условий не вырождения на fstIdx и head.

LaTeX

$$$$ cons\\, m\\, ls\\, h1\\, h2 = of m \\cdot ls $$$$

Lean4

@[simp]
theorem equivPair_tail {i} (p : Pair M i) : equivPair i p.tail = ⟨1, p.tail, p.fstIdx_ne⟩ :=
  equivPair_eq_of_fstIdx_ne _

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