prod_replicate — Mathlib

English

For any n ∈ ℕ and a in a monoid M, the product of n copies of a equals a^n.

Русский

Для любого n ∈ ℕ и элемента a из моноида M произведение n копий a равно a^n.

LaTeX

$$$(\mathrm{replicate}\ n\ a).prod = a^n$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_replicate (n : ℕ) (a : M) : (replicate n a).prod = a ^ n := by
  induction n with
  | zero => rw [pow_zero, replicate_zero, prod_nil]
  | succ n ih => rw [replicate_succ, prod_cons, ih, pow_succ']

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