p a b : ℕ
hpb : p ∈ factors b
ha : a ≠ 0
⊢ p ∈ factors (b * a)
p a b : ℕ
hpb : p ∈ factors b
ha : a ≠ 0
⊢ p ∈ factors (a * b)
rw [mul_comm]
no goals
p a b : ℕ
hpb : p ∈ factors b
ha : a ≠ 0
⊢ p ∈ factors (b * a)
exact mem_factors_mul_left hpb ha