mem_comap — Mathlib

English

For I a two-sided ideal of S and f a ring homomorphism, x ∈ I.comap f iff f(x) ∈ I.

Русский

Пусть I — двусторонний идеал кольца S, f — кольцевой гомоморфизм. Тогда x ∈ I comap f тогда и только тогда, когда f(x) ∈ I.

LaTeX

$$$ x \\in I^{\\mathrm{comap}(f)} \\iff f(x) \\in I $$$

Lean4

theorem mem_comap {I : TwoSidedIdeal S} {x : R} : x ∈ I.comap f ↔ f x ∈ I := by simp [comap, RingCon.comap, mem_iff]

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