Commit 2024-12-20 13:13 4bbcfacc

View on Github →

feat(RingTheory): HomogeneousLocalization.awayMap is a localization (#19486) This contribution was created as part of the Durham Computational Algebraic Geometry Workshop.

Estimated changes

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

added theorem HomogeneousLocalization.Away.isLocalization_mul

added theorem HomogeneousLocalization.Away.mk_surjective

added theorem HomogeneousLocalization.Away.val_mk

added theorem HomogeneousLocalization.awayMap_mk