uzpow_add

Mathlib.Data.ZMod.IntUnitsPower

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

English

Let s be a unit in the integers 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} \cdot s^{y} $$$

Lean4

theorem uzpow_add (s : ℤˣ) (x y : R) : s ^ (x + y) = s ^ x * s ^ y :=
  Additive.ofMul.injective <| add_smul x y (Additive.ofMul s)

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

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

Разделы

Аффилиация

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