to_additive, gpow, smul

Stream: maths

[Patrick Massot]

In this comment Sébastien naturally asks about deducing a lemma in additive group theory from the corresponding one for multiplicative groups. The reason we didn't do that is that to_additive currently doesn't handle translation of gpow which allows to write $g^n$ for $g$ in a multiplicative group and $n$ is an integer into the additive version gsmul allowing to write $ng$ where $g$ now belongs to an additive group. The definition is:

def gsmul (n : ℤ) (a : A) : A :=
@gpow (multiplicative A) _ a n

I guess this has been discussed before. Is it hopelessly out of scope for to_additive? Is there a reason not to want to_addtive to handle this? Or is it only that someone needs to go and add to_additive everywhere?

[Kevin Buzzard]

The issue is that the order of the variables changes

[Kevin Buzzard]

and right now that isn't supported

[Kevin Buzzard]

Maybe we could have [reducible] gsmul_aux a n := gsmul n a and then get it all working for aux and then just live with the corresponding reducible annoyance which presumably be like in the ge days

[Kevin Buzzard]

I don't know if to_additive could eat an abbreviation but maybe if it could then that would work better

[Reid Barton]

The lemma names also tend to have a corresponding permutation applied to their components, which might be tough for to_additive to replicate

[Yury G. Kudryashov]

And lemma arguments often come in different order.

[Yury G. Kudryashov]

Currently the standard way to get from pow/gpow to nsmul/gsmul is to apply the original lemma to @multiplicative α.

[Kevin Buzzard]

@Jason KY. I made you an unwitting recipient of an experiment with this. When we were setting up group theory from first principles I defined {{n}}^g to mean g^n because I wanted to see if anything felt more natural that way around. But I think it just ended up annoying you, right?

[Kevin Buzzard]

We could make Zsmul a right action?

[Kevin Buzzard]

It's not the same as smul, after all

[Patrick Massot]

@Sebastien Gouezel do you agree this all mean we should merge the subgroup PR without trying to fix this to_additive issue?

[Jason KY.]

Kevin Buzzard said:

Jason KY. I made you an unwitting recipient of an experiment with this. When we were setting up group theory from first principles I defined {{n}}^g to mean g^n because I wanted to see if anything felt more natural that way around. But I think it just ended up annoying you, right?

I didn't find the direction of the g and n to be annoying but the fact that I had to write the squiggly brackets every time!

[Sebastien Gouezel]

Yes, sure!