mathlib3
533f62f4 - chore(algebraic_geometry/open_immersion): split (#19149)

Commit
2 years ago
chore(algebraic_geometry/open_immersion): split (#19149) Split `algebraic_geometry/open_immersion` into a 1000-line file which doesn't mention schemes and a 1000-line file which does. This should open more porting targets (the first file should be available for porting immediately), but also helps towards a reorganization I have in mind for after-port: moving the [pre]sheafed-space and [locally-]ringed-space material from `algebraic_geometry` into a new folder in `topology` or `geometry`.
Author
Parents
Loading