head?_flatten_replicate — Mathlib

English

For any nonzero n, the head of the flatten of replicate n of l equals the head of l.

Русский

Для любого n ≠ 0 голова списка после расплющивания повторов равна голове l.

LaTeX

$$$$\\forall n:\\\\mathbb{N},\\\\ n \\neq 0 \\\\to \\\\forall l:\\\\mathrm{List}\\\\alpha,\n\\\\ \\mathrm{head?}(\\\\ \\mathrm{flatten}(\\\\ \\mathrm{replicate}(n,l))) = \\\\mathrm{head?}(l).$$$$

Lean4

@[simp]
theorem head?_flatten_replicate {n : ℕ} (h : n ≠ 0) (l : List α) : (List.replicate n l).flatten.head? = l.head? :=
  by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
  induction l <;> simp [replicate]

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