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