nsmul axioms of an additive group

Stream: mathlib4

[Antoine Chambert-Loir]

The definition of an additive commutative group contains the following field:

nsmul_succ : ∀ (n : ℕ) (x : G), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

Is it written like this on purpose, with the two terms switched, rather than the more obvious

nsmul_succ : ∀ (n : ℕ) (x : G), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x

[Eric Wieser]

I think it's written this way because for to_additive it is much easier if it matches docs#Group.npow_succ:

npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = x * Monoid.npow n x

[Eric Wieser]

I guess probably both could be changed

[Eric Wieser]

The other important thing is that the lemma is true by definition for docs#nsmulRec

[Antoine Chambert-Loir]

Of course that matches, but this is bizarre, and does not match with Nat.pow_succ, etc.

[Antoine Chambert-Loir]

nsmulRec should probably be changed in the same way…

[Eric Wieser]

I guess you could try changing it and seeing what breaks?

[Antoine Chambert-Loir]

OK.

[Antoine Chambert-Loir]

Oops, the file says:

-- use `x * npowRec n x` and not `npowRec n x * x` in the definition to make sure that
-- definitional unfolding of `npowRec` is blocked, to avoid deep recursion issues.

[Eric Wieser]

I have no idea what that means!

[Sébastien Gouëzel]

This dates back to Lean 3. I remember that npowRec n x * x created weird issues while x * npowRec n x didn't. It's possible that these issues have disappeared with Lean 4, so it's worth trying to see what happens!

[Antoine Chambert-Loir]

OK, so I try !

[Antoine Chambert-Loir]

I'm almost there, #11451, that was more painful than expected, especially because I exchanged the meanings of pow_succ and pow_succ' so that the unprimed version refers to the definition.