Commit 2024-11-27 18:07 6a0cdd15

View on Github →

feat(Algebra/Module): a presentation of an algebra induces a presentation of the module of differentials (#18440)

Estimated changes

Modified Mathlib.lean

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

added theorem Algebra.Presentation.differentials.comm₁₂

added theorem Algebra.Presentation.differentials.comm₁₂_single

added theorem Algebra.Presentation.differentials.comm₂₃'

added theorem Algebra.Presentation.differentials.comm₂₃

added theorem Algebra.Presentation.differentials.hom₁_single

added theorem Algebra.Presentation.differentials.surjective_hom₁

added theorem Algebra.Presentation.differentialsSolution_isPresentation