## Stream: maths

#### Patrick Massot (Oct 01 2020 at 15:43):

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 (Oct 01 2020 at 17:19):

The issue is that the order of the variables changes

#### Kevin Buzzard (Oct 01 2020 at 17:19):

and right now that isn't supported

#### Kevin Buzzard (Oct 01 2020 at 17:20):

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 (Oct 01 2020 at 17:21):

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

#### Reid Barton (Oct 01 2020 at 17:25):

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 (Oct 01 2020 at 17:54):

And lemma arguments often come in different order.

#### Yury G. Kudryashov (Oct 01 2020 at 17:55):

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

#### Kevin Buzzard (Oct 01 2020 at 18:01):

@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 (Oct 01 2020 at 18:01):

We could make Zsmul a right action?

#### Kevin Buzzard (Oct 01 2020 at 18:02):

It's not the same as smul, after all

#### Patrick Massot (Oct 01 2020 at 18:43):

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

#### Jason KY. (Oct 01 2020 at 19:50):

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 (Oct 01 2020 at 20:07):

Yes, sure!

Last updated: May 06 2021 at 17:38 UTC