pow_eq_prod_const

Mathlib.Algebra.BigOperators.Group.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.pow_eq_prod_const

English

For any natural number n and any commutative monoid M, the n-th power of b equals the product of n copies of b, i.e., b^n = ∏_{k=0}^{n-1} b.

Русский

Для любого натурального n и для любой коммутативной моноиды выполняется b^n = ∏_{k=0}^{n-1} b.

LaTeX

$$$b^{n} = \\prod_{k=0}^{n-1} b$$$

Lean4

@[to_additive]
theorem pow_eq_prod_const (b : M) : ∀ n, b ^ n = ∏ _k ∈ range n, b := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru