noncomputable def Real.emod (a b : ℝ) : ℝ

Equations

• a.emod b = Int.fract (a / b) * b

theorem Real.emod_in_interval {a b : ℝ} (hb : 0 < b) : a.emod b ∈ Set.Ico 0 b

theorem Real.emod_exists_multiple (a b : ℝ) (hb : 0 < b) : ∃ (k : ℤ), a.emod b = a + ↑k * b