prod_eq_pow_card — Mathlib

English

If every element of a list l equals a fixed element m, then l.prod = m^{|l|}.

Русский

Если каждый элемент списка l равен одному и тому же элементу m, то l.prod = m^{|l|}.

LaTeX

$$$\forall x \in l, x = m \Rightarrow l.prod = m^{|l|}$$$

Lean4

@[to_additive sum_eq_card_nsmul]
theorem prod_eq_pow_card (l : List M) (m : M) (h : ∀ x ∈ l, x = m) : l.prod = m ^ l.length := by
  rw [← prod_replicate, ← List.eq_replicate_iff.mpr ⟨rfl, h⟩]

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