Theorems · Theorem · number theory

NumberField.mixedEmbedding.polarSpaceCoord_apply

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (a : NumberField.mixedEmbedding.mixedSpace K),
  ↑(NumberField.mixedEmbedding.polarSpaceCoord K) a =
    (NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K) (a.1, Pi.map (fun i => ↑Complex.polarCoord) a.2)

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Cited by

0 results in Mathlib

Foundations

Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberField