preimageOfMemIntegerSet_mixedEmbedding

English

If x ∈ ring of integers and its image under mixedEmbedding lies in integerSet, then preimageOfMemIntegerSet applied to that image returns x.

Русский

Если x∈𝓞K и его образ под смешанным вложением лежит в integerSet, то preimageOfMemIntegerSet возвращает x.

LaTeX

$$If hx: mixedEmbedding(K) x ∈ integerSet(K) then preimageOfMemIntegerSet ⟨mixedEmbedding(K) x, hx⟩ = x.$$

Lean4

theorem preimageOfMemIntegerSet_mixedEmbedding {x : (𝓞 K)} (hx : mixedEmbedding K (x : 𝓞 K) ∈ integerSet K) :
    preimageOfMemIntegerSet (⟨mixedEmbedding K (x : 𝓞 K), hx⟩) = x := by
  simp_rw [RingOfIntegers.ext_iff, ← (mixedEmbedding_injective K).eq_iff, mixedEmbedding_preimageOfMemIntegerSet]

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