uzpow_sub

Mathlib.Data.ZMod.IntUnitsPower

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

English

Let s ∈ ℤˣ and x,y ∈ R. Then s^(x−y) = s^x / s^y.

Русский

Пусть s ∈ ℤˣ и x,y ∈ R. Тогда s^(x−y) = s^x / s^y.

LaTeX

$$$ \forall s \in \mathbb{Z}^{\times}, \forall x,y \in R,\ s^{x-y} = s^{x} / s^{y} $$$

Lean4

theorem uzpow_sub (s : ℤˣ) (x y : R) : s ^ (x - y) = s ^ x / s ^ y :=
  Additive.ofMul.injective <| sub_smul x y (Additive.ofMul s)

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

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

Разделы

Аффилиация

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