Configuration points lying on a polynomial factor
DefinitionEsgk_MaximallyCircularCurveDistinctDistancesalgebraic-geometryfinite-combinatoricsgeometry
This defines the subset of a finite configuration consisting of points that lie on the zero set of a chosen polynomial factor.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_Foundation
import Definitions.Def_Esgk_NormalizedFactorPointSelection
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
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
namespace Esgk
open PachDeZeeuw.Algebraic
def factorPointSet {n : ℕ} (p : Config n) (G : PlanePoly) :
Finset PachDeZeeuw.Algebraic.Point2 := by
classical
exact (factorPointIndices p G).image p
end Esgk