zpow_one_add₀

Mathlib.Algebra.GroupWithZero.Basic

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

English

If a ≠ 0, then for every integer i, a^{1+i} = a · a^{i}.

Русский

Если a ≠ 0, то для любого i: a^{1+i} = a · a^{i}.

LaTeX

$$$a \\\\neq 0 \\\\rightarrow \\\\forall i \\\\in \\\\mathbb{Z}, a^{1+i} = a \\\\cdot a^{i}$$$

Lean4

theorem zpow_one_add₀ (h : a ≠ 0) (i : ℤ) : a ^ (1 + i) = a * a ^ i := by rw [zpow_add₀ h, zpow_one]

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

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

Разделы

Аффилиация

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