English
In any ring, the negation distributes over multiplication on the left: −(a b) = a (−b).
Русский
Во всяком кольце отрицание распределяется по умножению слева: −(a b) = a(−b).
LaTeX
$$$-(a b) = a(-b)$$$
Lean4
/-- The auxiliary function takes real values for real arguments `x > 1`. -/
theorem LFunctionResidueClassAux_real (ha : IsUnit a) {x : ℝ} (hx : 1 < x) :
LFunctionResidueClassAux a x = (LFunctionResidueClassAux a x).re :=
by
rw [eqOn_LFunctionResidueClassAux ha hx]
simp only [sub_re, ofReal_sub]
congr 1
· rw [LSeries,
re_tsum <|
LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
(abscissaOfAbsConv_residueClass_le_one a).trans_lt <| by norm_cast]
push_cast
refine tsum_congr fun n ↦ ?_
rcases eq_or_ne n 0 with rfl | hn
· simp only [term_zero, zero_re, ofReal_zero]
· simp only [term_of_ne_zero hn, ← ofReal_natCast n, ← ofReal_cpow n.cast_nonneg, ← ofReal_div, ofReal_re]
· rw [← ofReal_natCast, ← ofReal_one, ← ofReal_sub, ← ofReal_inv, ← ofReal_div, ofReal_re]
