eq_rpow_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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