zpow_one_add

Mathlib.Algebra.Group.Basic

URI: https://scilib.ai/kg/mathlib#zpow_one_add

English

Let a be an element of a group G. For all integers n, a^(1+n) = a a^n.

Русский

Пусть a принадлежит группе G. Для всех целых n выполняется a^(1+n) = a a^n.

LaTeX

$$$\forall a \in G,\ \forall n \in \mathbb{Z},\ a^{1+n} = a\,a^{n}$$$

Lean4

@[to_additive one_add_zsmul]
theorem zpow_one_add (a : G) (n : ℤ) : a ^ (1 + n) = a * a ^ n := by rw [zpow_add, zpow_one]

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

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

Разделы

Аффилиация

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