prod_const — Mathlib

English

Let M be a commutative monoid. For any natural n and any element x ∈ M, the product over Fin(n) of the constant x equals x raised to the n-th power.

Русский

Пусть M — коммутативный моноид. При любом натуральном n и элементе x ∈ M произведение по Fin(n) константы x равно x^n.

LaTeX

$$$\displaystyle \prod_{i \in \mathrm{Fin}(n)} x = x^{n}$$$

Lean4

@[to_additive]
theorem prod_const (n : ℕ) (x : M) : ∏ _i : Fin n, x = x ^ n := by simp

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