coe_toReal — Mathlib

English

Let θ be an angle. Then the real number θ.toReal, viewed back as an angle, equals θ.

Русский

Пусть θ — угол. Тогда число θ.toReal, приведённое обратно к углу, равно θ.

LaTeX

$$$\\\\forall (\\\\theta : Real.Angle), \\\\(\\\\theta.toReal : Angle) = \\\\theta$$$

Lean4

@[simp]
theorem coe_toReal (θ : Angle) : (θ.toReal : Angle) = θ :=
  by
  induction θ using Real.Angle.induction_on
  exact coe_toIocMod _ _

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