mathlib
a9402e0a - refactor(algebraic_geometry/*): Make `LocallyRingedSpace.hom` a custom structure. (#15973)

Commit
3 years ago
refactor(algebraic_geometry/*): Make `LocallyRingedSpace.hom` a custom structure. (#15973) We also define `algebraic_geometry.Scheme.hom` as an type alias for morphisms between schemes to enable dot notation. Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Author
Parents
Loading