r : ℝ
hr : 0 < r
x : ℂ
hx : ↑abs x ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x
replace hx := Complex.abs.ne_zero_iff.mpr hx
no goals
r : ℝ
hr : 0 < r
x : ℂ
hx : ↑abs x ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x
simp_rw [log, map_mul, abs_ofReal, arg_real_mul _ hr, abs_of_pos hr, Real.log_mul hr.ne' hx,
  ofReal_add, add_assoc]