uzpow_neg

Mathlib.Data.ZMod.IntUnitsPower

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

English

Let s ∈ ℤˣ and x ∈ R. Then s^(−x) = (s^x)⁻¹.

Русский

Пусть s ∈ ℤˣ и x ∈ R. Тогда s^(−x) = (s^x)^{-1}.

LaTeX

$$$ \forall s \in \mathbb{Z}^{\times}, \forall x \in R,\ s^{-x} = (s^{x})^{-1} $$$

Lean4

theorem uzpow_neg (s : ℤˣ) (x : R) : s ^ (-x) = (s ^ x)⁻¹ :=
  Additive.ofMul.injective <| neg_smul x (Additive.ofMul s)

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

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

Разделы

Аффилиация

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