logDeriv_cos — Mathlib

English

The logarithmic derivative of the complex cosine is minus the tangent: logDeriv(Complex.cos) = -Complex.tan.

Русский

Логарифмическая производная косинуса комплексного равна минус тангенсу: logDeriv(Complex.cos) = -Complex.tan.

LaTeX

$$$\logDeriv(\mathrm{Complex}.\cos) = -\mathrm{Complex}.\tan$$$

Lean4

@[simp]
theorem logDeriv_cos : logDeriv (Complex.cos) = -Complex.tan :=
  by
  ext
  rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]

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