Theorem Module.FinitePresentation.iff_finitePresentation_of_finite

Modification history

2025-10-28 15:18
Mathlib/RingTheory/Finiteness/ModuleFinitePresentation.lean
feat(RingTheory/Finiteness): a finite and finitely presented algebra is finitely presented (#29781) …
Added Module.FinitePresentation.iff_finitePresentation_of_finiteView on Github →