L'Hopital's rule over any normed field

theorem norm_sub_norm_le_norm_add {E : Type u_1} [SeminormedAddGroup E] (x y : E) : ‖x‖ - ‖y‖ ≤ ‖x + y‖

theorem lhopital_field {𝕜 : Type} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {a f' g' : 𝕜} (df : HasDerivAt f f' a) (dg : HasDerivAt g g' a) (g'0 : g' ≠ 0) (f0 : f a = 0) (g0 : g a = 0) : Filter.Tendsto (fun (x : 𝕜) => f x / g x) (nhdsWithin a {a}ᶜ) (nhds (f' / g'))

L'Hôpital's rule using derivatives at a point, general field version