cotTerm_identity — Mathlib

English

Duplicate formulation: cotTerm equals 2x times reciprocal expression.

Русский

Дубликат формулы: cotTerm равен 2x умножить на обратное выражение.

LaTeX

$$$$\text{cotTerm}(x,n) = 2 x \cdot \frac{1}{(x + (n+1))(x - (n+1))}.$$$$

Lean4

theorem cotTerm_identity (hz : x ∈ ℂ_ℤ) (n : ℕ) : cotTerm x n = 2 * x * (1 / ((x + (n + 1)) * (x - (n + 1)))) :=
  by
  simp only [cotTerm]
  rw [one_div_add_one_div]
  · ring
  · simpa [sub_eq_add_neg] using integerComplement_add_ne_zero hz (-(n + 1) : ℤ)
  · simpa using (integerComplement_add_ne_zero hz ((n : ℤ) + 1))

Похожие утверждения