Translation center for a degree-two circular chart

Definition

Esgk_MaximallyCircularDegreeTwoCircle

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

algebraic-geometrycomplex-analysisgeometry

This defines the planar translation center associated with a complex isotropic parameter in the degree-two circular setting.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_PlaneCircleFactor
import Definitions.Def_LeanFormalizations_PachDeZeeuw_CurveInterface
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 MvPolynomial
open PachDeZeeuw.Algebraic

def bundle_Esgk_MaximallyCircularDegreeTwoCircle_isotropicTranslationCenter (ξ : ℂ) : _root_.Point2 :=
  WithLp.toLp 2 ![-ξ.re, -ξ.im]


end Esgk

View graph