tan_eq_sin_div_cos

Mathlib.Analysis.Complex.Trigonometric

URI: https://scilib.ai/kg/mathlib#Real.tan_eq_sin_div_cos

← MathLib Explorer

English

tan x = sin x / cos x for all real x (where cos x ≠ 0).

Русский

tan x = sin x / cos x для всех вещественных x (при cos x ≠ 0).

LaTeX

$$$ \tan x = \dfrac{\sin x}{\cos x} $$$

Lean4

nonrec theorem tan_eq_sin_div_cos : tan x = sin x / cos x :=
  ofReal_injective <| by simp only [ofReal_tan, tan_eq_sin_div_cos, ofReal_div, ofReal_sin, ofReal_cos]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru