cpow_ofNat_mul

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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