Theorem: nnnorm_circle_smul (PrimeNumberTheoremAnd/Fourier.lean)

State before:
z : ↥circle
s : ℂ
⊢ ‖z • s‖₊ = ‖s‖₊
Tactic:
simp [show z • s = z.val * s from rfl]
State after:
no goals