case mp
R : Type ?u.580497
n : ℕ
h : ↑μ n ≠ 0
⊢ Squarefree n

case mpr
R : Type ?u.580497
n : ℕ
h : Squarefree n
⊢ ↑μ n ≠ 0
R : Type ?u.580497
n : ℕ
⊢ ↑μ n ≠ 0 ↔ Squarefree n
constructor <;> intro h
case mp
R : Type ?u.580497
n : ℕ
h : ¬Squarefree n
⊢ ↑μ n = 0
case mp
R : Type ?u.580497
n : ℕ
h : ↑μ n ≠ 0
⊢ Squarefree n
contrapose! h
no goals
case mp
R : Type ?u.580497
n : ℕ
h : ¬Squarefree n
⊢ ↑μ n = 0
simp [h]
no goals
case mpr
R : Type ?u.580497
n : ℕ
h : Squarefree n
⊢ ↑μ n ≠ 0
simp [h, pow_ne_zero]