selfZPow_neg_mul

Mathlib.RingTheory.Localization.Away.Basic

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

English

The product selfZPow d times selfZPow (−d) equals 1.

Русский

Произведение selfZPow d и selfZPow (−d) равно 1.

LaTeX

$$$selfZPow(x,B,d) \cdot selfZPow(x,B,-d) = 1$$$

Lean4

theorem selfZPow_neg_mul (d : ℤ) : selfZPow x B (-d) * selfZPow x B d = 1 := by rw [mul_comm, selfZPow_mul_neg x B d]

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

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

Разделы

Аффилиация

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