Theorem Algebra.Presentation.differentialsSolution_isPresentation

Modification history

2024-11-27 18:07
Mathlib/Algebra/Module/Presentation/Differentials.lean
feat(Algebra/Module): a presentation of an algebra induces a presentation of the module of differentials (#18440)
Added Algebra.Presentation.differentialsSolution_isPresentationView on Github →