Theorems · Theorem · number theory

NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply

∀ (K : Type u_1) [inst : Field K] (x : NumberField.mixedEmbedding.realMixedSpace K),
  (NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K) x =
    (fun w => if hw : w.IsReal then x.1 ⟨w, hw⟩ else (x.2 ⟨w, ⋯⟩).1, fun w => (x.2 w).2)

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Cited by

0 results in Mathlib

Foundations

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

Assumes

Field