E : Type ?u.188465
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
r : ℚ
⊢ ‖↑↑r‖ = Abs.abs ↑r
E : Type ?u.188465
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
r : ℚ
⊢ ‖↑r‖ = Abs.abs ↑r
rw [← ofReal_rat_cast]
no goals
E : Type ?u.188465
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
r : ℚ
⊢ ‖↑↑r‖ = Abs.abs ↑r
exact norm_real _