replicate_succ_to_snoc

Mathlib.Data.Vector.Snoc

URI: https://scilib.ai/kg/mathlib#List.Vector.replicate_succ_to_snoc

← MathLib Explorer

English

replicate (n+1) val = (replicate n val).snoc val.

Русский

replicate (n+1) val = (replicate n val).snoc val.

LaTeX

$$$\operatorname{replicate}(n+1)\ val = (\operatorname{replicate} n\ val).snoc\ val$$$

Lean4

theorem replicate_succ_to_snoc (val : α) : replicate (n + 1) val = (replicate n val).snoc val := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [replicate_succ]
    conv => rhs; rw [replicate_succ]
    rw [snoc_cons, ih]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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