Commit 2026-06-25 19:06 68b30e53

feat: NSMul/NPow type class (#38036) This PR is adds NSMul, NPow, ZSMul and ZPow classes for the nsmul, npow, zsmul, zpow data fields. This has a few advantages:

• If you first declare a SMul instance, then you don't need to manually write nsmul := (· • ·) and zsmul := (· • ·) . For Pow, the extra benefit is that inferring the instance is preferred over the default field npowRecAuto. So this helps avoid accidental diamonds.
• If you first declare a SMul instance on a type synonym, then inferInstanceAs will infer the nsmul field from the SMul instance. This makes it easier to avoid diamonds on type synonyms like Matrix and MonoidAlgebra.
• The not-yet-merged instance diamond linter will be able to detect cases where the NSMul and SMul classes do not agree. In the process of making this PR, I have identified two existing NPow diamonds:
• In Mathlib.Algebra.Order.Positive.Field, there were two conflicting NPow instances.
• For Fin, there are two conflicting NPow instances. I have overwritten the one in core lean with the one from mathlib that is more computationally efficient. TODO: the same for QSMul and NNQSMul.