tan_coe

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

URI: https://scilib.ai/kg/mathlib#Real.Angle.tan_coe

English

For every real x, the tangent of x viewed as a real number equals the tangent of x as an angle.

Русский

Для каждого действительного x тангенс от x, считанного как число, равен тангенсу x как угла.

LaTeX

$$$\tan(x) = \tan x$$$

Lean4

@[simp]
theorem tan_coe (x : ℝ) : tan (x : Angle) = Real.tan x := by rw [tan, sin_coe, cos_coe, Real.tan_eq_sin_div_cos]

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

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

Разделы

Аффилиация

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