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

State before:
s : SelbergSieve
l : ℕ
hl : Squarefree l
⊢ μ l ^ 2 = 1
Tactic:
rw [moebius_apply_of_squarefree hl, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]
State after:
no goals