noncomputable def Formalization.maximalIdealAt {k : Type u_1} [Field k] {n : Type u_2} (p : n → k) : Ideal (MvPolynomial n k)

The maximal ideal of k[x_i]_i corresponding to a point p, generated by the linear forms X_i − p_i.

noncomputable def Formalization.hypersurfaceMultiplicityIdeal {k : Type u_1} [Field k] {n : Type u_2} (g : MvPolynomial n k) (p : n → k) : ℕ∞

Hypersurface multiplicity at a point (Def 12, Lec 5): the largest m such that the defining polynomial g lies in the m-th power of the maximal ideal at p — i.e., the lowest nonzero homogeneous degree of g expanded about p.