mul_uzpow

Mathlib.Data.ZMod.IntUnitsPower

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

← MathLib Explorer

English

The exponentiation distributes over multiplication of units: (s1 s2)^x = s1^x s2^x.

Русский

Возведение в степень распределяется по умножению единиц: (s1 s2)^x = s1^x s2^x.

LaTeX

$$$ (s_1 s_2)^x = s_1^x s_2^x.$$$

Lean4

theorem mul_uzpow (s₁ s₂ : ℤˣ) (x : R) : (s₁ * s₂) ^ x = s₁ ^ x * s₂ ^ x :=
  Additive.ofMul.injective <| smul_add x (Additive.ofMul s₁) (Additive.ofMul s₂)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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