Commit 2025-07-03 01:14 e7c314d3
View on Github →refactor: remove suppress_compilation from TensorProduct (#26642)
This was a workaround introduced in #7281 for extreme performance issues in the old compiler, which is no more!
This isn't an exhaustive removal of suppress_compilation, but is almost all of the ones related to TensorProduct.
A handful of noncomputables downstream can now be removed too.
Benchmark results seem mostly neutral.
Zulip thread: #mathlib4 > Why is tensor product noncomputable? @ 💬