normed and discrete_linear_ordered field

Stream: new members

[Anatole Dedecker]

Hello, I'm having some troubles working with a field that is both a normed_field and a discrete_linear_ordered_field : in the following mwe, the last line yields an error, which I interpret as "Lean doesn't know which field instance to use". What should I do to avoid this ?

import analysis.calculus.deriv

open filter asymptotics

open_locale topological_space

lemma tendsto_pow_div_pow {α : Type*} [normed_field α] [discrete_linear_ordered_field α]
  {p q : ℕ} (hpq : p < q) : is_o (λ (x : α), x^p) (λ x, x^q) at_top :=
begin
  rw is_o_iff_tendsto sorry,
  suffices h : tendsto (λ (x : α), x ^ ((p : ℤ) - q)) at_top (𝓝 0),
  { refine (tendsto_congr' ((eventually_gt_at_top (0 : α)).mono (λ x hx, _))).mp h,
    simp [fpow_sub hx.ne.symm] },
  rw ← neg_sub,
  rw ← int.coe_nat_sub hpq.le,
  have : 1 ≤ q - p := nat.sub_pos_of_lt hpq,
  exact @tendsto_pow_neg_at_top α _ _ (by apply_instance) _ this,
end

[Kenny Lau]

this is called a diamond

[Kenny Lau]

if you can't remove the diamond from the assumptions, create a new typeclass that merges the two

[Johan Commelin]

In other words, you'll need to define linear_ordered_normed_field

[Patrick Massot]

You can also do everything with real numbers and leave a TODO note saying that once someone will have cleaned the order hierarchy then this will be available for generalization.