Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-04-26 17:38
3e83c099
View on Github →
feat: Finitely Presented Modules (
#11870
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Algebra/Module/FinitePresentation.lean
added
theorem
Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule
added
theorem
Module.FinitePresentation.exists_lift_of_isLocalizedModule
added
theorem
Module.FinitePresentation.fg_ker
added
theorem
Module.FinitePresentation.fg_ker_iff
added
theorem
Module.FinitePresentation.isLocalizedModule_map
added
theorem
Module.finitePresentation_iff_finite
added
theorem
Module.finitePresentation_of_finite
added
theorem
Module.finitePresentation_of_free
added
theorem
Module.finitePresentation_of_free_of_surjective
added
theorem
Module.finitePresentation_of_ker
added
theorem
Module.finitePresentation_of_surjective
Modified
Mathlib/Algebra/Module/LocalizedModule.lean
added
theorem
IsLocalizedModule.lift_apply
added
def
IsLocalizedModule.map
added
theorem
IsLocalizedModule.map_apply
added
theorem
IsLocalizedModule.map_comp