Theorem IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation

Modification history

2026-01-22 12:40
Mathlib/Algebra/Module/FinitePresentation.lean
feat(RingTheory): predicate for `QuasiFiniteAt` (#33718)
Added IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentationView on Github →