The regular locus of a real plane curve
DefinitionEsgk_PlaneCurveRegularChartalgebraic-geometrygeometry
This defines the regular locus of a real polynomial plane curve by removing its singular points from its real zero set.
Definition code
-- Extracted dependency interfaces and their necessary proofs. import Definitions.Def_Esgk_PlaneCurveRadialChart import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim import Definitions.Def_LeanFormalizations_PachDeZeeuw_Bezout import Mathlib /- Copyright (c) 2026 Adam McKenna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Adam McKenna -/ noncomputable section open Set Filter Topology MvPolynomial open PachDeZeeuw.Algebraic namespace Esgk def planeCurveRegularLocus (G : PlanePoly) : Set Point2 := PlaneCurveZeroSet G \ SingularPointSet G end Esgk