feat: `NSMul`/`NPow` type class by JovanGerb · Pull Request #38036 · leanprover-community/mathlib4

JovanGerb · 2026-04-14T10:17:11Z

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.

github-actions · 2026-04-14T10:18:17Z

PR summary 4fceb4697e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ NPow
+ NPow.ofPow
+ NPow.toPow
+ NSMul
+ ZPow
+ ZPow.ofPow
+ ZPow.toPow
+ ZSMul
+ instance (n : ℕ) [NeZero n] : HPow (Fin n) ℕ (Fin n)
+ instance (n : ℕ) [NeZero n] : Pow (Fin n) ℕ
+ instance {A : Type*} [SMulZeroClass A R] : SMul A R[M]
- DivInvMonoid.toZPow
- Monoid.toPow
- SubNegMonoid.toZSMul
-++- addGroup

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

Decrease in tech debt: (relative, absolute) = (1.04, 0.03)

Current number	Change	Type
6219	1	backward.isDefEq.respectTransparency
795	-2	backward.privateInPublic
412	-1	backward.privateInPublic.warn
46	-1	dsimp +instances

Current commit dcf7b585bf
Reference commit 4fceb4697e

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

eric-wieser · 2026-04-14T18:06:40Z

Could you elaborate on the benefit here?

eric-wieser · 2026-04-14T23:18:37Z

If you first declare a SMul instance, then you don't need to manually write nsmul := (· • ·) and zsmul := (· • ·) .

This can also be achieved with [toNatSMul : SMul Nat A] as a field.

JovanGerb · 2026-04-14T23:21:14Z

Sure, but then you lose the ability to write nsmul := ..., and instead you have to write some awkward toNSMul := ⟨...⟩

vihdzp · 2026-04-15T00:24:39Z

 @[to_additive] instance addCommMonoid : AddCommMonoid R[M] :=
-  fast_instance% { (inferInstance : AddCommMonoid <| M →₀ R) with
-    nsmul n x := x.mapRange (n • ·) (smul_zero _) }
+  inferInstanceAs <| AddCommMonoid <| M →₀ R


What happened to fast_instance%?

This is the great thing: inferInstanceAs will automatically fill in the nsmul field using the smul that was was declared above. (Recall that inferInstanceAs and fast_instance% do the same kind of instance normalization). Previously, we had to awkwardly declare the nsmul field in order to avoid diamond.

I think this should also answer your other question: yes we do need to infer NSMul instances from SMul instances, for example here.

JovanGerb · 2026-04-15T09:34:56Z

!bench

leanprover-radar · 2026-04-15T09:35:16Z

Benchmark results for 12eaeea against 0446312 are in. There are significant results. @JovanGerb

🟥 build//instructions: +319.8G (+0.19%)

Large changes (1✅, 4🟥)

🟥 build/module/Mathlib.Analysis.CStarAlgebra.Fuglede//instructions: +20.8G (+40.83%)
🟥 build/module/Mathlib.Analysis.SpecialFunctions.Log.Deriv//instructions: +9.1G (+13.23%)
🟥 build/module/Mathlib.CategoryTheory.Triangulated.TriangleShift//instructions: +39.1G (+21.23%)
🟥 build/module/Mathlib.NumberTheory.Harmonic.GammaDeriv//instructions: +8.4G (+23.20%)
✅ build/module/Mathlib.RingTheory.Polynomial.UniversalFactorizationRing//instructions: -47.0G (-16.88%)

Medium changes (16✅, 10🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (39✅, 69🟥)

Too many entries to display here. View the full report on radar instead.

JovanGerb · 2026-04-15T22:06:11Z

!bench

leanprover-radar · 2026-04-15T22:06:32Z

Benchmark results for 604ad3b against 0446312 are in. There are significant results. @JovanGerb

🟥 build//instructions: +320.1G (+0.19%)

Large changes (1✅, 4🟥)

🟥 build/module/Mathlib.Analysis.CStarAlgebra.Fuglede//instructions: +20.8G (+40.81%)
🟥 build/module/Mathlib.Analysis.SpecialFunctions.Log.Deriv//instructions: +9.1G (+13.21%)
🟥 build/module/Mathlib.CategoryTheory.Triangulated.TriangleShift//instructions: +39.1G (+21.19%)
🟥 build/module/Mathlib.NumberTheory.Harmonic.GammaDeriv//instructions: +8.4G (+23.24%)
✅ build/module/Mathlib.RingTheory.Polynomial.UniversalFactorizationRing//instructions: -47.1G (-16.90%)

Medium changes (16✅, 11🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (38✅, 68🟥)

Too many entries to display here. View the full report on radar instead.

JovanGerb · 2026-04-15T22:29:13Z

It's curious how some files sped up while others slowed down. Maybe this change made some instances better - hence the speedup. But because of the extra extends, the structures are now a bit bigger, and hence unification takes longer (due to the exponentially slow unification thingy)

JovanGerb · 2026-04-20T20:02:06Z

!bench

leanprover-radar · 2026-04-20T20:02:25Z

Benchmark results for dcf7b58 against 4fceb46 are in. There are significant results. @JovanGerb

🟥 build//instructions: +319.9G (+0.18%)

Large changes (1✅, 4🟥)

🟥 build/module/Mathlib.Analysis.CStarAlgebra.Fuglede//instructions: +20.8G (+40.83%)
🟥 build/module/Mathlib.Analysis.SpecialFunctions.Log.Deriv//instructions: +9.1G (+13.25%)
🟥 build/module/Mathlib.CategoryTheory.Triangulated.TriangleShift//instructions: +38.3G (+20.71%)
🟥 build/module/Mathlib.NumberTheory.Harmonic.GammaDeriv//instructions: +8.3G (+23.04%)
✅ build/module/Mathlib.RingTheory.Polynomial.UniversalFactorizationRing//instructions: -50.3G (-16.96%)

Medium changes (14✅, 16🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (42✅, 69🟥)

Too many entries to display here. View the full report on radar instead.

jcommelin · 2026-04-21T13:55:28Z


 Note that `MulOpposite.smul` is provided in an earlier file as it is needed to
-provide the `AddMonoid.nsmul` and `AddCommGroup.zsmul` fields.
+provide the `NSMul.nsmul` and `AddCommGroup.zsmul` fields.


Should this be

Suggested change

provide the `NSMul.nsmul` and `AddCommGroup.zsmul` fields.

provide the `NSMul.nsmul` and `ZSMul.zsmul` fields.

jcommelin · 2026-04-21T13:57:00Z


 Note that `MulOpposite.smul` is provided in an earlier file as it is needed to
-provide the `AddMonoid.nsmul` and `AddCommGroup.zsmul` fields.
+provide the `NSMul.nsmul` and `AddCommGroup.zsmul` fields.


Suggested change

provide the `NSMul.nsmul` and `AddCommGroup.zsmul` fields.

provide the `NSMul.nsmul` and `ZSMul.zsmul` fields.

feat: NSMul/NPow type class

bccc247

JovanGerb added the WIP Work in progress label Apr 14, 2026

JovanGerb added 6 commits April 14, 2026 12:42

fix

041b901

use fast instance for Fin exponentiation

0d85eae

clean up that file

e34a60f

do the name for Int

86b4d32

fix

fa54279

fix

65e829c

JovanGerb added 3 commits April 14, 2026 23:21

use smul notation in the Prop fields

febb9c6

progress

ff1b9de

fix test

673fedc

JovanGerb added 2 commits April 15, 2026 01:36

.

a81983d

.

8fed238

vihdzp reviewed Apr 15, 2026

View reviewed changes

fixes

12eaeea

maybe faster?

604ad3b

Merge branch 'master' into Jovan-NSMul

dcf7b58

JovanGerb removed the WIP Work in progress label Apr 21, 2026

jcommelin reviewed Apr 21, 2026

View reviewed changes

	provide the `NSMul.nsmul` and `AddCommGroup.zsmul` fields.
	provide the `NSMul.nsmul` and `ZSMul.zsmul` fields.

Conversation

JovanGerb commented Apr 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Apr 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 4fceb4697e

Import changes for modified files

Declarations diff

Uh oh!

eric-wieser commented Apr 14, 2026

Uh oh!

eric-wieser commented Apr 14, 2026

Uh oh!

JovanGerb commented Apr 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

vihdzp Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

JovanGerb Apr 15, 2026

Choose a reason for hiding this comment

Uh oh!

JovanGerb commented Apr 15, 2026

Uh oh!

leanprover-radar commented Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JovanGerb commented Apr 15, 2026

Uh oh!

leanprover-radar commented Apr 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JovanGerb commented Apr 15, 2026

Uh oh!

JovanGerb commented Apr 20, 2026

Uh oh!

leanprover-radar commented Apr 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jcommelin Apr 21, 2026

Choose a reason for hiding this comment

Uh oh!

jcommelin Apr 21, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

JovanGerb commented Apr 14, 2026 •

edited

Loading

github-actions Bot commented Apr 14, 2026 •

edited

Loading

JovanGerb commented Apr 14, 2026 •

edited

Loading

leanprover-radar commented Apr 15, 2026 •

edited

Loading

leanprover-radar commented Apr 15, 2026 •

edited

Loading

leanprover-radar commented Apr 20, 2026 •

edited

Loading