2022-09-26 09:37
src/algebraic_geometry/projective_spectrum/scheme.lean
feat(algebraic_geometry/projective_spectrum/Scheme): the function from Spec to Proj restricted to basic open set. (#15259) …
Added algebraic_geometry.Proj_iso_Spec_Top_component.from_Spec.carrier.as_ideal