Generic lines detecting the order of a plane polynomial

A plane polynomial has a line of slope outside any prescribed finite set on which its analytic order equals its ambient order at a specified point. The first coordinate of the direction is fixed to one. This permits comparison with a ramified splitting in that coordinate without introducing a second power substitution.

theorem MvPolynomial.exists_analyticOrderAt_eval_finTwo_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (p : MvPolynomial (Fin 2) 𝕜) (hp : p ≠ 0) (a : Fin 2 → 𝕜) (s : Finset 𝕜) : ∃ c ∉ s, analyticOrderAt (fun (t : 𝕜) => (eval ![a 0 + t, a 1 + c * t]) p) 0 = p.orderAt a

A nonzero plane polynomial admits a line of slope outside any finite forbidden set that detects its ambient order at a specified point.