cpow_eq_pow

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

The complex power cpow x y coincides with the usual exponentiation x^y for complex x,y.

Русский

Комплексная степень cpow x y совпадает с обыкновенной степенью x^y для комплексных x,y.

LaTeX

$$$$ \text{cpow}(x,y) = x^{y} \quad \text{for all } x,y \in \mathbb{C}. $$$$

Lean4

@[simp]
theorem cpow_eq_pow (x y : ℂ) : cpow x y = x ^ y :=
  rfl

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

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

Разделы

Аффилиация

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