# Zulip Chat Archive

## Stream: general

### Topic: abel tactic

#### Mario Carneiro (Sep 10 2018 at 07:28):

Say hello to the `abel`

tactic, which does the same thing as `ring`

but for commutative additive monoids and commutative groups. It doesn't currently support `*`

on rings, since it would require a bit more support for `nat.cast`

and `int.cast`

in `norm_num`

, but otherwise it is full featured using `+`

, `-`

, and `add_monoid.smul`

, `gsmul`

.

I'm sure it won't be long before someone asks me to make a multiplicative version, I'll look into it. I plan to just use `additive`

to get the multiplicative version.

#### Patrick Massot (Sep 10 2018 at 07:31):

Great! How far is the module version then?

#### Mario Carneiro (Sep 10 2018 at 07:34):

The module version is basically a combination of `abel`

and `ring`

. It might be possible to generalize the coefficient ring to uniformize the treatment of additive groups as Z-modules, but we will need semimodules first, or else we will lose support for additive monoids with such a generalization

Last updated: May 10 2021 at 18:22 UTC