# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: group.div_self

#### Kevin Buzzard (Mar 12 2021 at 10:03):

Are we really missing these?

```
import algebra.group.hom
variables {A B : Type*} [group A] [group B]
(f : A →* B) (a1 a2 : A)
@[simp, to_additive] lemma group.div_self (a : A) : a / a = 1 :=
by simp [div_eq_mul_inv]
@[simp, to_additive] lemma monoid_hom.map_div :
f (a1 / a2) = f a1 / f a2 :=
by simp [div_eq_mul_inv]
```

I noticed there was a change to the definition of `group`

recently, with an explicit `div`

being asked for. This has turned out to work really nicely in group cohomology. I really don't want to write `g m + -m`

for a coboundary, and putting the emphasis on `add`

and `sub`

in general rather than `add`

and `neg`

seems to me like a good idea. Am I just not importing the right files for these two lemmas? Or is what's going on that `div`

is now being promoted as the new `inv`

but we didn't around to divifying everything yet?

PS `smul_sub`

is not tagged `simp`

. Is this for a good reason? Should `monoid_hom.map_div`

be `simp`

?

#### Anne Baanen (Mar 12 2021 at 10:08):

Or is what's going on that div is now being promoted as the new inv but we didn't around to divifying everything yet?

That is probably it. The old API was solely `mul`

and `inv`

based, with `sub`

only being defined for `add_group`

s. Now it's `div`

everywhere, but the lemmas haven't caught up yet.

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

is docs#smul_add tagged simp? edit: yes, so I guess smul_sub should be too

#### Kevin Buzzard (Mar 18 2021 at 10:55):

I was about to PR `map_div`

and I'm having second thoughts. I've realised that we *do* have `map_sub`

, which was what I wanted. I un-to-additived it and ended up with `map_div`

but I'm not sure that anyone really uses division in the non-commutative case.

#### Eric Wieser (Mar 18 2021 at 11:09):

I can't see any reason not to have the lemma

#### Kevin Buzzard (Mar 18 2021 at 12:02):

It opens up a can of worms in the noncommutative case.

#### Kevin Buzzard (Mar 18 2021 at 12:05):

Actually the real reason I don't want to PR it is that I don't need it. I needed `map_sub`

but it's there. There is this weird dichotomy amongst mathematicians. If they're using a structure which is commutative (as addition essentially always is in practice) then `sub`

is a powerful operator. If they're using a structure which is not (e.g. groups with group law `*`

are typically not commutative) then nobody uses `div`

at all because there are two potential definitions, but people will happily multiply by the inverse all day long.

Last updated: May 19 2021 at 02:10 UTC