cpow_sub

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

x^(y - z) = x^y / x^z (with x ≠ 0).

Русский

x^(y - z) = x^y / x^z (при x ≠ 0).

LaTeX

$$$$ x^{y - z} = \frac{x^{y}}{x^{z}} \quad (x \neq 0). $$$$

Lean4

theorem cpow_sub {x : ℂ} (y z : ℂ) (hx : x ≠ 0) : x ^ (y - z) = x ^ y / x ^ z := by
  rw [sub_eq_add_neg, cpow_add _ _ hx, cpow_neg, div_eq_mul_inv]

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

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

Разделы

Аффилиация

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