Inverse power mul

Stream: new members

[Colin Jones ⚛️]

What is the easiest way to prove this:

example (x : ℝ) : x⁻¹ ^ 2 = x ^ (-2:ℝ) := by
  simp only [inv_pow]

[Aaron Liu]

No idea if this is the "easiest"

import Mathlib

example (x : ℝ) : x⁻¹ ^ 2 = x ^ (-2:ℝ) := by
  conv => enter [2, 2]; equals Int.cast (-Nat.cast 2) => simp
  rw [Real.rpow_intCast, zpow_neg, zpow_natCast, inv_pow]

[Julian Berman]

import Mathlib
example (x : ℝ) : x⁻¹ ^ 2 = x ^ (-2:ℝ) := by
   norm_cast
   simp only [inv_pow, zpow_negSucc]

[Colin Jones ⚛️]

Thank you! How about this?

example (x : ℝ) (h : 0 < x) : x ^ (-10:ℝ) = 1 / x ^ (10:ℝ) := by
  rw?

[Edward van de Meent]

@loogle ?a ^ (-?b : Real), "rpow"

[loogle]

:search: Real.rpow_neg_one, Real.rpow_neg, and 30 more

[Edward van de Meent]

docs#Real.rpow_neg, docs#Real.inv_rpow, and docs#inv_eq_one_div should help you here. Depending on the operator precedence, you may not need the second one.