cpow_mul_ofNat

Mathlib.Analysis.SpecialFunctions.Pow.Complex

URI: https://scilib.ai/kg/mathlib#Complex.cpow_mul_ofNat

English

Let x, y ∈ ℂ and n ∈ ℕ. Then x^(y·ofNat(n)) = (x^y)^(ofNat(n)).

Русский

Пусть x, y ∈ ℂ и n ∈ ℕ. Тогда x^(y·ofNat(n)) = (x^y)^(ofNat(n)).

LaTeX

$$$x^{y \cdot \mathrm{ofNat}(n)} = (x^{y})^{\mathrm{ofNat}(n)}$$$

Lean4

theorem cpow_mul_ofNat (x y : ℂ) (n : ℕ) [n.AtLeastTwo] : x ^ (y * ofNat(n)) = (x ^ y) ^ ofNat(n) :=
  cpow_mul_nat x y n

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

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

Разделы

Аффилиация

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