A polynomial detecting failure of shear separation

Definition

LeanFormalizations_PachDeZeeuw_CrossingLemma_ShearExists

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrygeometry

For two planar points, this defines the linear polynomial whose value at a shear parameter is the difference of their first coordinates after the shear.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_LeanFormalizations_PachDeZeeuw_CrossingLemma_ShearIrreducible
import Definitions.Def_LeanFormalizations_PachDeZeeuw_CrossingLemma_ShearPartialY
import Mathlib

set_option autoImplicit true

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


namespace PachDeZeeuw.Algebraic

open MvPolynomial


noncomputable def sepPoly (p q : ℝ × ℝ) : Polynomial ℝ :=
  Polynomial.C (p.1 - q.1) - Polynomial.C (p.2 - q.2) * Polynomial.X


end PachDeZeeuw.Algebraic

View graph