norm_cast
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ m then ↑(μ d) else 0) = if l = m then ↑(μ l) else 0
P : ℕ
hP : Squarefree P
l m : ℕ
hm : m ∣ P
⊢ (∑ x ∈ P.divisors, if l ∣ x ∧ x ∣ m then μ x else 0) = if l = m then μ l else 0