Theorem Module.Finite.of_isLocalization

Modification history

2026-03-03 14:56
Mathlib/RingTheory/Localization/Finiteness.lean
chore(RingTheory): reorganize imports around locality properties of finiteness (#36044)
Modified Module.Finite.of_isLocalizationView on Github →
2025-07-15 11:35
Mathlib/RingTheory/RingHom/Finite.lean
feat: add Mathlib.RingTheory.DedekindDomain.Instances (#26070) …
Added Module.Finite.of_isLocalizationView on Github →