localization_comap_range — Mathlib

English

The range of comap (algebraMap R S) equals the set of primes p with disjointness from M.

Русский

Образ comap (algebraMap R S) равен множеству простых идеалов p, которые дисjoint с M.

LaTeX

$$Set.range (comap (algebraMap R S)) = {p | Disjoint (M : Set R) p.asIdeal}.$$

Lean4

theorem localization_comap_range [Algebra R S] (M : Submonoid R) [IsLocalization M S] :
    Set.range (comap (algebraMap R S)) = {p | Disjoint (M : Set R) p.asIdeal} :=
  localization_specComap_range ..

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