E : Type ?u.222428
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ ^ n = 1 ^ n
E : Type ?u.222428
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ = 1
refine' (@pow_left_inj NNReal _ _ _ _ zero_le' zero_le' hn.bot_lt).mp _
no goals
E : Type ?u.222428
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ ^ n = 1 ^ n
rw [← nnnorm_pow, h, nnnorm_one, one_pow]