Real.mod

Stream: Is there code for X?

[Casavaca]

Is there Real.mod? how can I do something like

abbrev Rad : Type := { x : ℝ // 0 ≤ x ∧ x < 2*π }
def ofReal : ℝ → Rad := fun x ↦ Real.mod x (2 * π)

[Yuyang Zhao]

docs#Real.Angle.toReal might help.

[Yuyang Zhao]

import Mathlib

open Set Real

abbrev Rad : Type := Ico 0 (2*π)
noncomputable def Rad.ofReal : ℝ → Rad :=
  fun x ↦ ⟨toIcoMod two_pi_pos _ x, toIcoMod_mem_Ico' two_pi_pos _⟩

[Yaël Dillies]

You are looking for docs#toIcoMod