No has_lt typeclass instance for rational number

Stream: new members

[Mukesh Tiwari]

Below is the code, which makes Lean typechecker unhappy:

import data.nat.basic
  data.rat.basic

def neg_fn (μ : ℕ → ℚ) : Prop :=
  ∀ (c : ℕ), ∃ (n₀ : ℕ),
    ∀ (n : ℕ), n ≥ n₀ → (μ n) * (n ^ c) < 1

and the error I am getting is:
failed to synthesize type class instance for has_lt ℚ:

μ : ℕ → ℚ,
c n₀ n : ℕ,
a : n ≥ n₀
⊢ has_lt ℚ

By looking at the documentation [1], I see there is no has_lt instance for rationals. However, the error goes away if I import data.real.basic (but not changing anything else). So my questions are:

1. why there is not has_lt typeclass for rationals (is there something I am missing obvious)?
2. when I am import data.real.basic, is ℚ is coerced to ℝ?

[1] https://leanprover-community.github.io/mathlib_docs/data/rat/basic.html

[Johan Commelin]

@Mukesh Tiwari https://leanprover-community.github.io/mathlib_docs/data/rat/order.html

[Mukesh Tiwari]

@Johan Commelin Thank you very much.

[Jalex Stark]

Imports are transitive

[Jalex Stark]

So you import the file that Johan pointed to when you say import data.real.basic