Theorems · Theorem · commutative algebra
Ideal.IsMaximal.of_isLocalization_of_disjoint
∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_4} [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] [IsLocalization M S] {J : Ideal S} [(Ideal.under R J).IsMaximal], J.IsMaximal- Cited by
- 2 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Top.topproof · cited by 9,680
- Idealstatement and proof · cited by 4,748
- Algebra.algebraMapproof · cited by 4,706
- Submonoidstatement and proof · cited by 3,086
- Ideal.mapproof · cited by 692
- IsLocalizationstatement and proof · cited by 636
- Ideal.IsMaximalstatement and proof · cited by 452
- Ideal.understatement and proof · cited by 170
- Ideal.IsPrime.ne_topproof · cited by 82
- Ideal.exists_le_maximalproof · cited by 47
Cited by2
Results whose statement or proof uses this declaration.
- IsLocalization.isMaximal_iff_isMaximal_disjointproof · cited by 3
- Polynomial.height_eq_height_add_oneproof · cited by 1