Commit 2026-05-22 10:01 8e98f824
View on Github →feat(LinearAlgebra/QuadraticForm): generalize discr (#39415)
This generalizes QuadraticMap.discr, which currently takes Q : QuadraticMap R (n → R) R to QuadraticForm.discr b, which allows Q : QuadraticForm R M where M is an R-module with a finite R-basis b.
The old versions are preserved since the generalizations are noncomputable, but their names are updated: QuadraticMap is replaced by QuadraticForm and QuadraticMap.discr is renamed to QuadraticForm.discr' (continuing with the notation convention LinearMap.toMatrix' vs LinearMap.toMatrix).