Theorem: nnnorm_eq_of_mem_circle (PrimeNumberTheoremAnd/Fourier.lean)

State before:
z : ↥circle
⊢ ↑‖↑z‖₊ = 1
Tactic:
simp
State after:
no goals