Theorem: Real.inv_eq_pow_neg_one (CvxLean/Lib/Math/Data/Real.lean)

State before:
a : ℝ
ha : 0 < a
⊢ a⁻¹ = a ^ (-1)
Tactic:
rw [inv_eq_one_div, one_div_eq_pow_neg_one ha]
State after:
no goals