Signs and compact angular coordinates in the mixed embedding space

noncomputable def NairTenenbaum.mixedPolarCoordinates {K : Type u_1} [Field K] (σ : { w : NumberField.InfinitePlace K // w.IsReal } → Bool) (r : NumberField.mixedEmbedding.realSpace K) (a : { w : NumberField.InfinitePlace K // w.IsComplex } → ℝ) : NumberField.mixedEmbedding.mixedSpace K

Real and complex polar coordinates for the archimedean embeddings.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.exists_mixedPolarCoordinates {K : Type u_1} [Field K] (x : NumberField.mixedEmbedding.mixedSpace K) : ∃ (σ : { w : NumberField.InfinitePlace K // w.IsReal } → Bool), ∃ a ∈ Set.Icc (fun (x : { w : NumberField.InfinitePlace K // w.IsComplex }) => 0) fun (x : { w : NumberField.InfinitePlace K // w.IsComplex }) => 1, mixedPolarCoordinates σ (NumberField.mixedEmbedding.normAtAllPlaces x) a = x