Commit 2024-07-20 11:05 70d37777
View on Github →feat: BilinForm.toQuadraticForm is surjective in free modules (#14292)
That is: if your module is free, you can always write Q = B.toQuadraticMap, which means that the base change exists.
This doesn't go as far as changing QuadraticForm.baseChange, as this would trade one generality (Invertible (2 : R)) for another (Module.Free R M).