Commit 2026-05-04 12:17 7fcea958

perf: raise prio of various Mul->SMul instances (#38704) The instances instSMulOfMul /instVAddOfAdd, MulZeroClass.toSMulWithZero, Monoid.toMulAction / AddMonoid.toAddAction, MonoidWithZero.toMulActionWithZero and Semiring.toModule are all of the form F X -> G X X (so rarely apply) and are essentially always the right choice when they do apply (I know of no counterexample, in fact). They are also all at lowered priority on master, a decision which came from mathlib3 (which had a very different algorithm for typeclass inference). I have raised them to higher priority than default (in fact to 1100) and this causes a speedup of around 20% in several of the slowest files in mathlib (Mathlib.RingTheory.Etale.QuasiFinite, Mathlib.RingTheory.DedekindDomain.Different, Mathlib.RingTheory.ZariskisMainTheorem,...) and a general speedup in far more files.