Commit 2023-09-20 09:16 f2ec396b
View on Github →perf: make QuadraticForm.tensorDistrib noncomputable (#7265)
It's actually (trivially) computable, but Lean takes such an extraordinarily long time to compile it that its better to pretend that it isn't.
Another instance of #7103.