## Stream: maths

### Topic: abel multiplication

#### Patrick Massot (May 29 2019 at 17:26):

It seems that abel works only for add_comm_group, not for comm_group. @Mario Carneiro, would that be easy to fix?

#### Mario Carneiro (May 29 2019 at 17:27):

It would basically need to apply additive to turn it into a multiplicative problem

#### Patrick Massot (May 29 2019 at 17:34):

Is it something you may do in the near future?

#### Mario Carneiro (May 29 2019 at 17:35):

not today. I'll look into it

Thanks!

#### Amelia Livingston (Nov 21 2019 at 20:30):

How would applying additive in a proof work in practice? I tried to do this a few months ago (so can't really remember how it went) but the only way I could get to work reliably in a use case where I wanted to be in tactic mode was to add the lemma

lemma to_add {α} [has_mul α] :


and rw to_add as needed, which I liked because it wasn't too many extra characters, but is there a proper way?

#### Mario Carneiro (Nov 21 2019 at 21:44):

The intended use is to write out the desired statement directly, and apply the corresponding multiplicative theorem and have defeq work out the differences. algebra.group_power has a few examples with multiplicative

#### Amelia Livingston (Dec 08 2019 at 03:51):

(deleted, I found something that works)

#### Bryan Gin-ge Chen (Mar 07 2021 at 21:10):

I'd like to use abel for inf and sup in (semi)lattices. I'm envisioning using it to reorder / reassociate terms in e.g. a calc block before doing more rewriting. How hard would it be to generalize abel to this use case? I'm thinking of doing this in two steps: first set up some wrapper(s) like additive and then try to figure out if abel can be generalized to additive semigroups (since semilattices may not have top or bot).

For the first step, am I right that we can't reuse additive directly since all the instances are already set up to go to / from has_mul? Is there some more generic approach?

#### Eric Wieser (Mar 07 2021 at 21:11):

src#additive.has_add is implemented in terms of has_mul, so yes, you'd can't reuse that one and would need a new one

#### Bryan Gin-ge Chen (Mar 07 2021 at 21:13):

Hmm, maybe I should wait for #6045 to be merged before attempting this...

#### Alex J. Best (Mar 07 2021 at 21:20):

Yeah, that looks like what I had in mind! I think I should be able to set things up so I can write change statements like the examples you posted, but then abel requires add_comm_monoid which I might not have.