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_finite'View on Github →