toIocMod_toReal — Mathlib

English

The real value of θ is fixed by θ.toReal with respect to the modulo operation: toIocMod two_pi_pos (-π) θ.toReal = θ.toReal.

Русский

Реальное значение θ ограничено модульной операцией: toIocMod two_pi_pos (-π) θ.toReal = θ.toReal.

LaTeX

$$$\\\\forall (\\\\theta : Real.Angle), \\\\text{toIocMod } two\_pi\_pos (-\\\\pi) \\\\theta.toReal = \\\\theta.toReal$$$

Lean4

@[simp]
theorem toIocMod_toReal (θ : Angle) : toIocMod two_pi_pos (-π) θ.toReal = θ.toReal :=
  by
  induction θ using Real.Angle.induction_on
  rw [toReal_coe]
  exact toIocMod_toIocMod _ _ _ _

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