mathlib3

583ad823 - feat(algebraic_geometry/structure_sheaf): Structure sheaf on basic opens (#7405)

feat(algebraic_geometry/structure_sheaf): Structure sheaf on basic opens (#7405) Proves that `to_basic_open` is an isomorphism of commutative rings. Also adds Hartshorne as a reference. Co-authored-by: Justus Springer <justusspringer@gmx.de>