The detector module kills every nonunit

import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Algebra.Polynomial.Expand
import Mathlib.Algebra.Polynomial.Taylor
import Mathlib.RingTheory.PicardGroup
import Mathlib.LinearAlgebra.DirectSum.TensorProduct
import Definitions.Def_RybinP18_CuspidalCubicInput

open WeierstrassCurve
open WeierstrassCurve.Affine
open Polynomial
open scoped Polynomial.Bivariate
open scoped DirectSum

namespace CuspidalCubicInput

noncomputable section





















































































lemma detectorModule_kills_nonunits :
    ∀ a : cusp.CoordinateRing, ¬ IsUnit a →
      ∃ m : detectorModule, m ≠ 0 ∧ a • m = 0 := by
  sorry

end
end CuspidalCubicInput