preimageOfMemIntegerSet — Mathlib

English

If x is the preimage corresponding to a ∈ integerSet, then its embedding under mixedEmbedding matches a.

Русский

Если x — пр образ a ∈ integerSet, то его образ под смешанным вложением даёт a.

LaTeX

$$mixedEmbedding(K) (preimageOfMemIntegerSet a) = a.$$

Lean4

/-- 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`. -/
def preimageOfMemIntegerSet (a : integerSet K) : (𝓞 K)⁰ :=
  ⟨(mem_integerSet.mp a.prop).2.choose,
    mem_nonZeroDivisors_of_ne_zero
      (by
        simp_rw [ne_eq, ← RingOfIntegers.coe_injective.eq_iff, ← (mixedEmbedding_injective K).eq_iff, map_zero,
          (mem_integerSet.mp a.prop).2.choose_spec, ne_zero_of_mem_integerSet, not_false_eq_true])⟩

Похожие утверждения