x y : ℝ
hx_nonneg : 0 ≤ x
⊢ abs (x ^ y) = abs x ^ y
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ ‖x ^ y‖ = ‖x‖ ^ y
simp_rw [Real.norm_eq_abs]
no goals
x y : ℝ
hx_nonneg : 0 ≤ x
⊢ abs (x ^ y) = abs x ^ y
exact abs_rpow_of_nonneg hx_nonneg