zpow_neg_mul_zpow_self

Mathlib.Algebra.GroupWithZero.Units.Basic

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

English

For any a ≠ 0 and integer n, the product a^{-n} a^{n} equals 1.

Русский

Для любого a ≠ 0 и целого n выполняется a^{-n} a^{n} = 1.

LaTeX

$$$\forall a\neq 0,\forall n\in\mathbb{Z}: a^{-n} a^{n} = 1$$$

Lean4

theorem zpow_neg_mul_zpow_self (n : ℤ) (ha : a ≠ 0) : a ^ (-n) * a ^ n = 1 := by rw [zpow_neg];
  exact inv_mul_cancel₀ (zpow_ne_zero n ha)

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

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

Разделы

Аффилиация

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