Theorem HomogeneousLocalization.Away.val_mk

Modification history

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