to_additive translating pow to nsmul

Stream: mathlib4

[Ruben Van de Velde]

It seems like mathlib3 to_additive can translate pow to nsmul rather than smul (e.g. docs#set.nsmul_subset_nsmul), but mathlib4 doesn't. Is that known?

[Yaël Dillies]

Nevermind, I can't read

[Floris van Doorn]

In Lean 3 we had the translations

pow -> nsmul
npow -> nsmul
zpow -> zsmul

This is a bit inconsistent, and in many files we translate pow to smul, so I tried changing the translation in mathlib4: pow -> smul. This was probably a bad idea without backporting the change. Shall I change it back to pow -> nsmul in mathlib4?
Do we have an idea whether we have more lemmas that we want to be called nsmul than lemmas that want to be called smul?

[Floris van Doorn]

I opened mathlib4#1502 as WIP PR

[Eric Wieser]

I woudl expect the vast majority want to be called nsmul, there are vanishingly few places where the pow operator is generalized to more than just nat

[Eric Wieser]

(docs#pi.has_pow is the only one that comes to mind)

[Floris van Doorn]

But we're not consistent in always calling (n : ℕ) • _ nsmul and _ ^ (n : ℕ) pow. But you're probably right anyway, that the Lean 3 heuristic matches the current lemma names much better.

[Eric Wieser]

My claim would be that that inconsistency is accidental not deliberate, and we should fix such cases when we find them

[Floris van Doorn]

I'll try to flag such inconsistencies in mathlib4#1502. After that is merged, someone can go through the comments and change the names.

[Floris van Doorn]

I think I fixed all errors in mathlib4#1502, which is now ready for review