Theorems · Definition · number theory

NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet

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

For a : integerSet K, the unique nonzero algebraic integer x such that its image by mixedEmbedding is equal to a. Note that we state the fact that x ≠ 0 by saying that x is a nonzero divisors since we will use later on the isomorphism Ideal.associatesNonZeroDivisorsEquivIsPrincipal, see integerSetEquiv.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Cited by

14 results in Mathlib

Foundations

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

Assumes

FieldNumberField