Theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left

Modification history

2024-11-20 19:44
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
feat(AlgebraicGeometry): Proj is separated (#19290) …
Added AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_leftView on Github →