Commit 2024-09-17 21:38 3b220c58
View on Github →feat(RingTheory/StandardSmooth): ring isomorphisms are standard smooth (#16869)
We show that any R-algebra S where algebraMap R S is bijective, is standard smooth by constructing an explicit submersive presentation.
This contribution was created as part of the AIM workshop "Formalizing algebraic geometry"
in June 2024.