Theorem HomogeneousLocalization.Away.mk_surjective

Modification history

2024-12-20 13:13
Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
feat(RingTheory): `HomogeneousLocalization.awayMap` is a localization (#19486) …
Added HomogeneousLocalization.Away.mk_surjectiveView on Github →