Commit 2025-04-10 11:43 9b20cb5f
View on Github →chore(RingTheory/StandardSmooth): fix SubmersivePresentation.basisCotangent (#23776)
The current basis is not what the docstring claims to be: It is the basis given by pre-images of the standard basis of P.rels → S, which don't agree with the images of P.relation i in P.toExtension.Cotangent.