pow_succ

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.pow_succ

English

For any submodule M and natural n, the (n+1)-st power is the product of the n-th power with M: M^(n+1) = M^n · M.

Русский

Для подмодуля M и натурального n выполняется M^(n+1) = M^n · M.

LaTeX

$$$M^{(n+1)} = M^n \cdot M$$$

Lean4

protected theorem pow_succ {n : ℕ} : M ^ (n + 1) = M ^ n * M :=
  rfl

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

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

Разделы

Аффилиация

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