Commit 2024-11-04 07:19 079e5ca5

feat(Algebra/Module): the tautological presentation of a module (#18374) Any A-module M admits a tautological presentation by generators and relation. There is a generator [m] for any element m : M, and there are two types of relations:

• [m₁] + [m₂] - [m₁ + m₂] = 0
• a • [m] - [a • m] = 0.