algebraMap_mem_map_algebraMap_iff

English

An element algebraMap x lies in a mapped ideal iff there exists a witness in M such that m x is in I.

Русский

Элемент algebraMap x лежит в образе идеала тогда и только тогда, существует m в M, такое что m x ∈ I.

LaTeX

$$algebraMap_mem_map_algebraMap_iff I x$$

Lean4

theorem algebraMap_mem_map_algebraMap_iff (I : Ideal R) (x : R) :
    algebraMap R S x ∈ I.map (algebraMap R S) ↔ ∃ m ∈ M, m * x ∈ I := by
  rw [← IsLocalization.mk'_one (M := M), mk'_mem_map_algebraMap_iff]

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