rpow_neg_eq_inv_rpow — Mathlib

English

For nonnegative x and any real y, x^(-y) = (x^y)^{-1}.

Русский

При неотрицательном x и любом y вещественном выполняется x^{-y} = (x^{y})^{-1}.

LaTeX

$$$x \ge 0 \Rightarrow \forall y \in \mathbb{R},\ x^{-y} = (x^{y})^{-1}$$$

Lean4

/-- See also `rpow_neg` for a version with `(x ^ y)⁻¹` in the RHS. -/
theorem rpow_neg_eq_inv_rpow (x y : ℝ) : x ^ (-y) = x⁻¹ ^ y := by
  simp [rpow_def, Complex.cpow_neg, Complex.inv_cpow_eq_ite, apply_ite]

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