Theorems · Theorem · number theory

NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.normAtAllPlaces '' NumberField.mixedEmbedding.fundamentalCone.normLeOne K =
    ⇑NumberField.mixedEmbedding.mixedSpaceOfRealSpace ⁻¹'
            NumberField.mixedEmbedding.logMap ⁻¹'
              ZSpan.fundamentalDomain
                (Module.Basis.ofZLatticeBasis ℝ (NumberField.Units.unitLattice K)
                  (NumberField.Units.basisUnitLattice K)) ∩
          {x | ∀ (w : NumberField.InfinitePlace K), 0 ≤ x w} ∩
        {x | NumberField.mixedEmbedding.norm (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) ≠ 0} ∩
      {x | NumberField.mixedEmbedding.norm (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) ≤ 1}

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField