Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 08:55 f7d7a91c

View on Github →

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.

Estimated changes