Theorems · Theorem · commutative algebra

IsLocalization.minimalPrimes_comap

∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A] (J : Ideal A),
  (Ideal.comap (algebraMap R A) J).minimalPrimes = Ideal.comap (algebraMap R A) '' J.minimalPrimes

Defined in: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Cited by: 1 results in Mathlib
Foundations: Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring CommSemiring Algebra IsLocalization

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
RingHomstatement · cited by 10,189
Set.imagestatement and proof · cited by 5,609
Set.preimageproof · cited by 4,946
Idealstatement and proof · cited by 4,748
Algebra.algebraMapstatement and proof · cited by 4,706
Submonoidstatement and proof · cited by 3,086
IsLocalizationstatement and proof · cited by 636
Ideal.comapstatement and proof · cited by 443
Ideal.underproof · cited by 170

Cited by1

Results whose statement or proof uses this declaration.

IsLocalization.height_underproof · cited by 6