Theorem Algebra.Presentation.differentials.surjective_hom₁

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.differentials.surjective_hom₁View on Github →