ofReal_cot — Mathlib

English

Let x be a real number. The complex cotangent of x, obtained by viewing the real cotangent in the complex plane, coincides with the real cotangent function. In other words, Real.cot x, regarded as a complex number, equals cot x.

Русский

Пусть x является вещественным числом. Комплексный котангенс x, полученный как вещественный котангенс, рассмотренный как элемент ℂ, совпадает с вещественным котангенсом x. Иными словами, (Real.cot x : ℂ) = cot x.

LaTeX

$$$\\forall x \\in \\mathbb{R},\\; (\\mathrm{Real.cot}\\ x : \\mathbb{C}) = \\cot x$$$

Lean4

@[simp, norm_cast]
theorem ofReal_cot (x : ℝ) : (Real.cot x : ℂ) = cot x :=
  ofReal_cot_ofReal_re _

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