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

State before:
a : ℝ
ha : 0 < a
⊢ 1 / a = a ^ (-1)
Tactic:
rw [rpow_neg (le_of_lt ha), rpow_one, div_eq_mul_inv, one_mul]
State after:
no goals