isChain_cons_eq_iff_eq_replicate — Mathlib

English

For any a and l, the chain of a :: l under equality holds if and only if l is a replication of a by its length.

Русский

Для любого a и l цепь равенства для списка a :: l существует тогда, когда хвост l повторяет a требуемой длины.

LaTeX

$$$IsChain(=)(a::l)\\iff l=Replicate(|l|)\\ a$$$

Lean4

theorem isChain_cons_eq_iff_eq_replicate {a : α} {l : List α} : IsChain (· = ·) (a :: l) ↔ l = replicate l.length a :=
  by simp [isChain_eq_iff_eq_replicate, replicate_succ]

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