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

State before:
x : ℝ
⊢ (-x).exp = 1 / x.exp
Tactic:
rw [exp_neg, inv_eq_one_div]
State after:
no goals