zpow_sub

Mathlib.Algebra.Group.Basic

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

English

For all a ∈ G and m,n ∈ ℤ, a^{m-n} = a^m a^{-n}.

Русский

Для всех a ∈ G и m,n ∈ ℤ, a^{m-n} = a^{m} a^{-n}.

LaTeX

$$$\forall a \in G,\ \forall m,n \in \mathbb{Z},\ a^{m-n} = a^{m} a^{-n}$$$

Lean4

@[to_additive sub_zsmul]
theorem zpow_sub (a : G) (m n : ℤ) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ := by rw [Int.sub_eq_add_neg, zpow_add, zpow_neg]

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

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

Разделы

Аффилиация

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