cpow_neg

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

x^(-y) = (x^y)^{-1}.

Русский

x^(-y) = (x^y)^{-1}.

LaTeX

$$$$ x^{-y} = (x^{y})^{-1}. $$$$

Lean4

theorem cpow_neg (x y : ℂ) : x ^ (-y) = (x ^ y)⁻¹ :=
  by
  simp only [cpow_def, neg_eq_zero, mul_neg]
  split_ifs <;> simp [exp_neg]

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

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

Разделы

Аффилиация

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