def IntersectionMultSingular.evalAtPoint (k : Type u_1) [Field k] (a b : k) : MvPolynomial (Fin 2) k →+* k

Evaluation ring homomorphism at the point (a, b) ∈ k².

def IntersectionMultSingular.PointOnCurve (k : Type u_1) [Field k] (f : MvPolynomial (Fin 2) k) (a b : k) : Prop

Predicate: the point (a, b) lies on the curve f = 0.

def IntersectionMultSingular.IsSingularAt (k : Type u_1) [Field k] (f : MvPolynomial (Fin 2) k) (a b : k) : Prop

A plane curve f is singular at (a, b) if both partial derivatives vanish at the point and the point lies on the curve.

theorem IntersectionMultSingular.intersection_mult_ge_two_of_singular (k : Type u_1) [Field k] (f g : MvPolynomial (Fin 2) k) (a b : k) (hf : f ≠ 0) (hg : g ≠ 0) (hX : PointOnCurve k f a b) (hY : PointOnCurve k g a b) (hSing : IsSingularAt k f a b ∨ IsSingularAt k g a b) : LocalIntersection.localIntersectionMultiplicity k f g a b ≥ 2

Corollary 20: if one of the two plane curves f, g is singular at a common point (a, b), the local intersection multiplicity at that point is at least two.