rpow_inv_eq — Mathlib

English

For nonnegative x,y and nonzero z, x^{z^{-1}} = y iff x = y^{z}.

Русский

Для неотрицательных x, y и не нулевого z верно: x^{z^{-1}} = y эквивалентно x = y^{z}.

LaTeX

$$$0 \le x \land 0 \le y \land z \neq 0 \Rightarrow x^{z^{-1}} = y \iff x = y^{z}$$$

Lean4

theorem rpow_inv_eq (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : z ≠ 0) : x ^ z⁻¹ = y ↔ x = y ^ z := by
  rw [← rpow_left_inj _ hy hz, rpow_inv_rpow hx hz]; positivity

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