Theorem IsLocalization.Away.span_range_mulNumerator_eq_top

Modification history

2024-10-04 10:12
Mathlib/RingTheory/Localization/Away/Lemmas.lean
feat(RingTheory): target local closure of property of ring homomorphisms (#17032) …
Added IsLocalization.Away.span_range_mulNumerator_eq_topView on Github →