Commit 2024-11-04 07:19 00a70aba

View on Github →

feat(Algebra/Module): presentation of a direct sum of modules (#18359) Given a family of A-modules M i and a presentation of each M i, we construct a presentation of ⨁ i, M i.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Presentation/Basic.lean

added def Module.Presentation.ofLinearEquiv

deleted theorem Module.Relations.Solution.IsPresentation.ofLinearEquiv

added theorem Module.Relations.Solution.IsPresentation.of_linearEquiv

Created Mathlib/Algebra/Module/Presentation/DirectSum.lean

added theorem Module.Presentation.directSum_var

added theorem Module.Presentation.finsupp_var

added theorem Module.Relations.Solution.IsPresentation.directSum

added def Module.Relations.Solution.directSum

added def Module.Relations.Solution.directSumEquiv

added theorem Module.Relations.Solution.directSum_var

Modified Mathlib/Algebra/Module/Presentation/Free.lean