Def Algebra.Generators.PresentationOfFreeCotangent.Aux.basisRight

Modification history

2025-12-05 16:31

Mathlib/RingTheory/Extension/Cotangent/Basis.lean

feat(RingTheory/Extension/Cotangent): basis of free cotangent space can be realized as a presentation (#31034) …

Added Algebra.Generators.PresentationOfFreeCotangent.Aux.basisRight View on Github →