mathlib

f7d7a91c - feat(algebraic_geometry/ringed_space): Define basic opens for ringed spaces. (#9358)

feat(algebraic_geometry/ringed_space): Define basic opens for ringed spaces. (#9358) Defines the category of ringed spaces, as an alias for `SheafedSpace CommRing`. We provide basic lemmas about sections being units in the stalk and define basic opens in this context.