Theorem: LSeries.term_mul_aux (EulerProducts/EulerProduct.lean)

State before:
a b : ℂ
m n : ℕ
s : ℂ
⊢ a / ↑m ^ s * (b / ↑n ^ s) = a * b / (↑m * ↑n) ^ s
Tactic:
rw [mul_comm_div, div_div, ← mul_div_assoc, mul_comm (m : ℂ), natCast_mul_natCast_cpow]
State after:
no goals