α : Type u_1
β : Type ?u.2595
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, b = a * b_1) ↔ a ∣ b
α : Type u_1
β : Type ?u.2595
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, -b = a * ↑(Equiv.neg α).symm b_1) ↔ a ∣ b
simp
no goals
α : Type u_1
β : Type ?u.2595
inst✝¹ : Semigroup α
inst✝ : HasDistribNeg α
a b c : α
⊢ (∃ b_1, b = a * b_1) ↔ a ∣ b
rfl