Theorem Module.finitePresentation_of_projective_of_exact

Modification history

2025-01-25 16:37
Mathlib/Algebra/Module/FinitePresentation.lean
feat(RingTheory): the smooth locus of an algebra (#20953)
Added Module.finitePresentation_of_projective_of_exactView on Github →