Theorem: SelbergSieve.abs_moebius_eq_one_of_squarefree (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean)

State before:
s : SelbergSieve
l : ℕ
hl : Squarefree l
⊢ |μ l| = 1
Tactic:
simp only [moebius_apply_of_squarefree hl, abs_pow, abs_neg, abs_one, one_pow]
State after:
no goals