Theorems · Definition · number theory

NumberField.mixedEmbedding.polarCoordReal

(K : Type u_1) →
  [inst : Field K] →
    [NumberField K] →
      OpenPartialHomeomorph (NumberField.mixedEmbedding.realMixedSpace K) (NumberField.mixedEmbedding.realMixedSpace K)

The polar coordinate open partial homeomorphism of ℝ^r₁ × (ℝ × ℝ)^r₂ defined as the identity on the first component and mapping (rᵢ cos θᵢ, rᵢ sin θᵢ)ᵢ to (rᵢ, θᵢ)ᵢ on the second component.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Cited by

13 results in Mathlib

Foundations

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

Assumes

FieldNumberField