ordered_module ℚ ℝ

Stream: Is there code for X?

[Yakov Pechersky]

What's the right generality to provide the instance that would give the instance here:

import algebra.module.ordered
import data.real.sqrt

instance : ordered_module ℚ ℝ := sorry

[Yakov Pechersky]

I don't need it directly, but came across it missing during debugging. In particular, it would make shorter proofs here:

example (q : ℚ) (x y : ℝ) (hq : 0 ≤ q) (h : x ≤ y) :
  q • x ≤ q • y :=
begin
  have : ∀ (r : ℝ), q • r = (q : ℝ) * r := λ _, rfl,
  rw [this, this],
  refine mul_le_mul_of_nonneg_left h _,
  simpa using hq
end

example (q : ℚ) (x y : ℝ) (hq : 0 ≤ q) (h : x ≤ y) :
  q • x ≤ q • y :=
smul_le_smul_of_nonneg h hq -- doesn't work without instance