feat(analysis/exponential): pow_nat_rpow_nat_inv

src/analysis/exponential.lean

@@ -1115,6 +1115,9 @@ begin
     (complex.of_real_mul _ _).symm, -complex.of_real_mul] at *
 end
 
+@[simp] lemma abs_cpow_inv_nat (x : ℂ) (n : ℕ) : abs (x ^ (n⁻¹ : ℂ)) = x.abs ^ (n⁻¹ : ℝ) :=
+by rw ← abs_cpow_real; simp [-abs_cpow_real]
+
 end complex
 
 namespace real
@@ -1152,4 +1155,9 @@ by simp only [rpow_def, (complex.of_real_pow _ _).symm, complex.cpow_nat_cast,
 by simp only [rpow_def, (complex.of_real_fpow _ _).symm, complex.cpow_int_cast,
   complex.of_real_int_cast, complex.of_real_re]
 
+lemma pow_nat_rpow_nat_inv {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : 0 < n) : 
+  (x ^ n) ^ (n⁻¹ : ℝ) = x :=
+have hn0 : (n : ℝ) ≠ 0, by simpa [nat.pos_iff_ne_zero'] using hn,
+by rw [← rpow_nat_cast, ← rpow_mul hx, mul_inv_cancel hn0, rpow_one]
+
 end real