Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-01 07:45 73f50ac6

View on Github →

feat(algebraic_geometry): Redefine Schemes in terms of isos of locally ringed spaces (#8888) Addresses the project mentioned in Scheme.lean to redefine Schemes in terms of isomorphisms of locally ringed spaces, instead of presheafed spaces.

Estimated changes