Theorem Module.Finite.of_localizationSpan_finite

Modification history

2024-06-23 21:54
Mathlib/RingTheory/Localization/Finiteness.lean
feat(RingTheory): localization and finiteness (#14054) …
Added Module.Finite.of_localizationSpan_finiteView on Github →