reduce_replicate — Mathlib

English

Reducing a word that is a repetition of a block leaves the block unchanged: reduce(replicate n x) = replicate n x.

Русский

Редукция слова, повторяющего блок, не изменяет повторяемый блок: reduce(replicate n x) = replicate n x.

LaTeX

$$$$\operatorname{reduce}(\mathrm{replicate}\ n\ x) = \mathrm{replicate}\ n\ x.$$$$

Lean4

@[to_additive (attr := simp)]
theorem reduce_replicate (n : ℕ) (x : α × Bool) : reduce (.replicate n x) = .replicate n x := by
  induction n with
  | zero => simp [reduce]
  | succ n ih =>
    rw [List.replicate_succ, reduce.cons, ih]
    cases n with
    | zero => simp
    | succ n => simp [List.replicate_succ]

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