p a b : ℕ
hab : coprime a b
hpb : p ∈ factors b
⊢ ↑(factorization (b * a)) p = ↑(factorization b) p
p a b : ℕ
hab : coprime a b
hpb : p ∈ factors b
⊢ ↑(factorization (a * b)) p = ↑(factorization b) p
rw [mul_comm]
no goals
p a b : ℕ
hab : coprime a b
hpb : p ∈ factors b
⊢ ↑(factorization (b * a)) p = ↑(factorization b) p
exact factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb