zpow_negSucc

Mathlib.Algebra.Group.Defs

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

English

For a ∈ G and n ∈ ℕ, a^{−(n+1)} = (a^{n+1})^{-1}.

Русский

Для a ∈ G и n ∈ ℕ: a^{−(n+1)} = (a^{n+1})^{-1}.

LaTeX

$$$a^{-(n+1)} = (a^{n+1})^{-1}$$$

Lean4

theorem zpow_negSucc (a : G) (n : ℕ) : a ^ (Int.negSucc n) = (a ^ (n + 1))⁻¹ :=
  by
  rw [← zpow_natCast]
  exact DivInvMonoid.zpow_neg' n a

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

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

Разделы

Аффилиация

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