Theorems · Definition · number theory

NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates

(K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K) →
        Associates ↥(nonZeroDivisors (NumberField.RingOfIntegers K))

The map that sends an element of a : integerSet K to the associates class of its preimage in (𝓞 K)⁰. By quotienting by the kernel of the map, which is equal to the subgroup of torsion, we get the equivalence integerSetQuotEquivAssociates.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldNumberField