theorem proved term proof

`rpow_inv_hom'`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  75theorem rpow_inv_hom' (α : ℝ) {x : ℝ} (hx : 0 < x) :
  76    x⁻¹ ^ α = (x ^ α)⁻¹ := by

Term-mode proof.

  77  rw [rpow_def_of_pos (inv_pos.mpr hx), rpow_def_of_pos hx,
  78      log_inv, neg_mul, exp_neg]
  79
  80/-! ## Calibration Invariance -/
  81

Lean names referenced from this declaration's body.