m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 2 = 1
⊢ 1 ≠ 0
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 2 = 1
⊢ Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 2 ≠ 0
rw [Hpv]
no goals
m : ℤ
hm : 0 < m
p : ℕ
hp : Fact (Nat.Prime p)
Hpv : Part.get (multiplicity (↑p) m) (_ : multiplicity.Finite (↑p) m) % 2 = 1
⊢ 1 ≠ 0
exact one_ne_zero