toReal_pi

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

English

The real value of π as an angle is π: (π : Angle).toReal = π.

Русский

Реальное значение π как угла равно π: (π : Angle).toReal = π.

LaTeX

$$$\\\\forall \\\$\\\\angle = (\\\\pi : Angle)\\\$, \\\\(\\\\angle.toReal) = \\\\pi$$$

Lean4

@[simp]
theorem toReal_pi : (π : Angle).toReal = π := by
  rw [toReal_coe_eq_self_iff]
  exact ⟨Left.neg_lt_self Real.pi_pos, le_refl _⟩

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

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

Разделы

Аффилиация

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