Theorems · Theorem · commutative algebra
Algebra.Smooth.of_formallySmooth_fiber
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
[Algebra.FinitePresentation R S],
(∀ (I : Ideal R) [inst_5 : I.IsPrime], Algebra.FormallySmooth I.ResidueField (I.Fiber S)) → Algebra.Smooth R S- Defined in
- Mathlib.RingTheory.Smooth.Fiber
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 139 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Idealstatement and proof · cited by 4,748
- Ideal.IsPrimestatement and proof · cited by 827
- PrimeSpectrumproof · cited by 625
- Ideal.primeComplstatement · cited by 462
- PrimeSpectrum.asIdealproof · cited by 333
- Localization.AtPrimestatement · cited by 299
- Module.Flatstatement and proof · cited by 279
- Ideal.underproof · cited by 170
- IsLocalRing.ResidueFieldstatement · cited by 156
- Ideal.ResidueFieldstatement and proof · cited by 119
Cited by2
Results whose statement or proof uses this declaration.
- Algebra.Etale.of_formallyUnramified_of_flatproof · cited by 2
- AlgebraicGeometry.Smooth.of_smooth_fiberToSpecResidueFieldproof · cited by 0