coe_real_pi

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

URI: https://scilib.ai/kg/mathlib#NNReal.coe_real_pi

English

The real embedding of the NNReal π agrees with the real π.

Русский

Переход π из NNReal в ℝ совпадает с числом π в ℝ.

LaTeX

$$$\operatorname{toReal}(\pi_{\mathrm{NNReal}}) = \pi$$$

Lean4

@[simp]
theorem coe_real_pi : (pi : ℝ) = π :=
  rfl

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

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

Разделы

Аффилиация

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