Prove2Me

Real and imaginary coefficient projections

Definition
Esgk_NonabsolutePlanePointBound

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

algebracomplex-analysispolynomials

This maps a complex plane polynomial to the real plane polynomials obtained by taking the real part or imaginary part of every coefficient.

Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_PlaneNonabsoluteRealPointBound
import Definitions.Def_Esgk_PlaneProjectiveHomogenization
import Definitions.Def_Esgk_PlaneProjectiveModel
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
open scoped ComplexConjugate

 
def complexRealPartPoly (H : ComplexPlanePoly) : PlanePoly :=
  AddMonoidAlgebra.ofCoeff
    (Finsupp.mapRange Complex.re (by simp) (AddMonoidAlgebra.coeff H))

 
def complexImagPartPoly (H : ComplexPlanePoly) : PlanePoly :=
  AddMonoidAlgebra.ofCoeff
    (Finsupp.mapRange Complex.im (by simp) (AddMonoidAlgebra.coeff H))


end Esgk

View graph