no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hdvd : a ∣ b
heq : 0 = multiplicity a b
⊢ multiplicity a b < 1
simpa only [heq, Nat.cast_zero] using PartENat.coe_lt_coe.mpr zero_lt_one
no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
hdvd : a ∣ b
heq : 0 = multiplicity a b
⊢ a ^ 1 ∣ b
rwa [pow_one a]