Theorem HomogeneousLocalization.Away.isLocalization_mul

Modification history

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