Michael Stoll

```text General information: lint: -1.5075 * 10⁹ (-0.0126%) build: -9.1613 * 10⁹ (-0.00783%) Files that got slower by at least 10⁹ instructions: Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm: +1.8527 * 10⁹ (+0.666%) No file got...

General information: ```text lint: +23.963 * 10⁹ (+0.299%) build: +114.28 * 10⁹ (+0.0933%) ``` 15 files got slower by at least 10⁹ instructions ```text Mathlib.LinearAlgebra.QuadraticForm.Basic: +42.057 * 10⁹ (+30.1%) Mathlib.LinearAlgebra.ExteriorAlgebra.Grading:...

My script reports: ```text General information: lint: -34.605 * 10⁹ (-0.288%) build: -320.41 * 10⁹ (-0.277%) Files that got slower: Mathlib.AlgebraicTopology.SimplicialObject: +2.0389 * 10⁹ (+0.995%) Mathlib.Algebra.Homology.HomotopyCategory.Triangulated: +1.4258 * 10⁹ (+0.734%)...

Some more statistics (extracted from the last comparison): ```text lint: -463.96 * 10⁹ (-3.80%) build: -6036.9 * 10⁹ (-5.10%) Files that got slower: Mathlib.CategoryTheory.Preadditive.EilenbergMoore: +8.1559 * 10⁹ (+3.44%) Mathlib.RepresentationTheory.Action.Basic: +3.9758...

maintainer merge

General information: ```text lint: +3.5755 * 10⁹ (+0.0445%) build: +49.877 * 10⁹ (+0.0406%) ``` 7 files got slower by at least 10⁹ instructions: ```text Mathlib.LinearAlgebra.Matrix.SesquilinearForm: +35.147 * 10⁹ (+31.4%) Mathlib.LinearAlgebra.Matrix.BilinearForm:...

Maybe I should have put everything together in one big "suggestion" comment. It looks like it works after all changes are made (I had checked out your branch and changed...

maintainer merge

Late to the party, but here are more detailed results from the comparison above: ```text General information: lint: -260.80 * 10⁹ (-2.16%) build: -161.69 * 10⁹ (-0.139%) No file got...

Some of the `ring_nf`s were a bit slow because of the fairly involved expressions occurring. Abstracting the relevant atoms via `generalize` gives a noticeable speed-up.