Theorem Algebra.Presentation.Generators.fg_ker_of_finitePresentation

Modification history

2025-12-05 16:31
Mathlib/RingTheory/Extension/Presentation/Basic.lean
feat(RingTheory/Extension/Cotangent): basis of free cotangent space can be realized as a presentation (#31034) …
Added Algebra.Presentation.Generators.fg_ker_of_finitePresentationView on Github →