## Stream: new members

### Topic: normed and discrete_linear_ordered field

#### Anatole Dedecker (Oct 26 2020 at 10:07):

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 (Oct 26 2020 at 11:12):

this is called a diamond

#### Kenny Lau (Oct 26 2020 at 11:13):

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

#### Johan Commelin (Oct 26 2020 at 12:02):

In other words, you'll need to define linear_ordered_normed_field

#### Patrick Massot (Oct 26 2020 at 13:23):

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.

Last updated: May 10 2021 at 23:11 UTC