minimalPrimes_comap_subset — Mathlib

English

For any f and J, (J.comap f).minimalPrimes is contained in the image of J.minimalPrimes under comap f.

Русский

Для произвольного f и J: (J.comap f).minimalPrimes ⊆ comap f '' J.minimalPrimes.

LaTeX

$$$ (J.comap f).minimalPrimes \subseteq Ideal.comap f '' J.minimalPrimes $$$

Lean4

theorem minimalPrimes_comap_subset (f : R →+* S) (J : Ideal S) :
    (J.comap f).minimalPrimes ⊆ Ideal.comap f '' J.minimalPrimes := fun p hp ↦
  Ideal.exists_minimalPrimes_comap_eq f p hp

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