Theorem HomogeneousLocalization.awayMap_fromZeroRingHom

Modification history

2024-11-20 19:44
Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
feat(AlgebraicGeometry): Proj is separated (#19290) …
Added HomogeneousLocalization.awayMap_fromZeroRingHomView on Github →