K : Type u_1
E : Type ?u.6572189
inst✝ : IsROrC K
n : ℕ
⊢ ‖↑↑n‖ = ↑n
K : Type u_1
E : Type ?u.6572189
inst✝ : IsROrC K
n : ℕ
⊢ ‖↑n‖ = ↑n
rw [← ofReal_natCast]
no goals
K : Type u_1
E : Type ?u.6572189
inst✝ : IsROrC K
n : ℕ
⊢ ‖↑↑n‖ = ↑n
exact norm_of_nonneg (Nat.cast_nonneg n)