cpow_nat_mul

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

For any x, y ∈ ℂ and n ∈ ℕ, x^(n y) = (x^y)^n.

Русский

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

LaTeX

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

Lean4

theorem cpow_nat_mul (x : ℂ) (n : ℕ) (y : ℂ) : x ^ (n * y) = (x ^ y) ^ n :=
  mod_cast cpow_int_mul x n y

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

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

Разделы

Аффилиация

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