2022-07-11 14:26
src/algebraic_geometry/projective_spectrum/scheme.lean
feat(algebraic_geometry/projective_spectrum): forward direction of homeomorphism between top_space of Proj and top_space of Spec (#13397) …
Added algebraic_geometry.Proj_iso_Spec_Top_component.to_Spec.carrier