pow_mk — Mathlib

English

For any natural n, the n-th power of mk L equals mk of the flattened n-fold replication of L.

Русский

Для любого натурального n степень n элемента mk L равна mk(сплющиванию n раз L).

LaTeX

$$$\\mk L\\,^n = \\mk(\\text{List.flatten}(\\text{List.replicate } n\\; L))$$$

Lean4

@[to_additive (attr := simp)]
theorem pow_mk (n : ℕ) : mk L ^ n = mk (List.flatten <| List.replicate n L) :=
  match n with
  | 0 => rfl
  | n + 1 => by rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]

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