no goals
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
⊢ (multiplicity a (-b)).Dom ↔ (multiplicity a b).Dom
simp only [multiplicity, PartENat.find, dvd_neg]
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h₁ : (multiplicity a (-b)).Dom
h₂ : (multiplicity a b).Dom
⊢ multiplicity a (-b) = ↑(Part.get (multiplicity a b) h₂)
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h₁ : (multiplicity a (-b)).Dom
h₂ : (multiplicity a b).Dom
⊢ ↑(Part.get (multiplicity a (-b)) h₁) = ↑(Part.get (multiplicity a b) h₂)
rw [PartENat.natCast_get]
no goals
α : Type u_1
inst✝¹ : Ring α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
h₁ : (multiplicity a (-b)).Dom
h₂ : (multiplicity a b).Dom
⊢ multiplicity a (-b) = ↑(Part.get (multiplicity a b) h₂)
exact Eq.symm
        (unique (pow_multiplicity_dvd _).neg_right
          (mt dvd_neg.1 (is_greatest' _ (lt_succ_self _))))