instPow

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

The power operation on complex numbers agrees with cpow, i.e., for all x,y, cpow(x,y) = x^y.

Русский

Степенная операция над комплексными числами согласуется с cpow, то есть для любых x,y выполняется cpow(x,y) = x^y.

LaTeX

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

Lean4

noncomputable instance : Pow ℂ ℂ :=
  ⟨cpow⟩

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

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

Разделы

Аффилиация

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