Theorem HomogeneousLocalization.awayMap_mk

Modification history

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