Theorems · Definition · number theory

NumberField.mixedEmbedding.fundamentalCone.idealSetEquivNorm

(K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) →
        (n : ℕ) →
          { a // NumberField.mixedEmbedding.norm ↑a = ↑n } ≃
            { I // ↑J ∣ ↑I ∧ Submodule.IsPrincipal ↑I ∧ Ideal.absNorm ↑I = n } × ↥(NumberField.Units.torsion K)

For an integer n, The equivalence between the elements of idealSet K of norm n and the product of the set of nonzero principal ideals of K divisible by J of norm n and the torsion of K.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField