mathlib3
94b96cff - feat(algebraic_geometry/structure_sheaf): stalk_iso (#4047)

Commit
5 years ago
feat(algebraic_geometry/structure_sheaf): stalk_iso (#4047) Given a ring `R` and a prime ideal `p`, construct an isomorphism of rings between the stalk of the structure sheaf of `R` at `p` and the localization of `R` at `p`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Author
Parents
Loading