Theorems · Theorem · commutative algebra
IsLocalization.Away.finitePresentation
∀ {R : Type u_1} [inst : CommRing R] (r : R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
[IsLocalization.Away r S], Algebra.FinitePresentation R S- Cited by
- 7 results in Mathlib
- Foundations
- Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- AlgEquiv.symmproof · cited by 615
- Submonoid.powersproof · cited by 408
- IsLocalization.Awaystatement and proof · cited by 218
- Localization.Awayproof · cited by 162
- AlgEquiv.transproof · cited by 108
- Algebra.FinitePresentationstatement · cited by 56
- IsLocalization.algEquivproof · cited by 45
- Algebra.FinitePresentation.equivproof · cited by 9
- Localization.awayEquivAdjoinproof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- RingHom.Smooth.holdsForLocalizationAwayproof · cited by 2
- Algebra.isOpen_smoothLocusproof · cited by 2
- Algebra.FinitePresentation.of_isLocalizationAwayproof · cited by 1
- RingHom.finitePresentation_holdsForLocalizationAwayproof · cited by 1
- Algebra.Smooth.of_isLocalization_Awayproof · cited by 0
- Algebra.Etale.of_isLocalizationAwayproof · cited by 0
- Algebra.basicOpen_subset_smoothLocus_iff_smoothproof · cited by 0