Theorems · Theorem · number theory

NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {a : NumberField.mixedEmbedding.mixedSpace K},
  a ∈ NumberField.mixedEmbedding.fundamentalCone.integerSet K → ∃! x, (NumberField.mixedEmbedding K) ↑x = a

If a is in integerSet, then there is a unique algebraic integer in 𝓞 K such that mixedEmbedding K x = a.

Defined in

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldNumberField