# Zulip Chat Archive

## Stream: maths

### Topic: gpowers

#### Kevin Buzzard (Jul 24 2020 at 12:28):

Currently if g is in a group, `gpowers g`

is the subset {gpow g n | n : int} and it's a theorem that this is a `is_subgroup`

. I'm removing `is_subgroup`

from mathlib in a branch (and it's really good fun, it's got to the point where most of the refactoring is high-powered stuff and it's fun to fix the proofs). I tried replacing gpowers g with the subgroup closure of the singleton g, but the underlying set is now not defeq to the g^n and I'm constantly having to rewrite. How about I rename gpowers (the subgroup generated by g as a set) to gpowers.carrier and redefine gpowers g to be the subgroup, with carrier defeq to the powers of g? Is the set really more important than the subgroup?

#### Scott Morrison (Jul 24 2020 at 12:32):

Yeah, `gpowers`

should certainly be the `subgroup`

.

#### Mario Carneiro (Jul 24 2020 at 12:58):

I don't think `gpowers.carrier`

needs a name at all. Just call it `(gpowers g : set g)`

#### Kevin Buzzard (Jul 24 2020 at 14:23):

I see!

#### Chris Hughes (Jul 24 2020 at 15:55):

I think I remember making `subgroup.gpowers`

a while ago.

#### Kevin Buzzard (Jul 24 2020 at 16:54):

I'll take a look. There's certainly an is_subgroup gpowers

#### Yury G. Kudryashov (Jul 24 2020 at 19:56):

Note that in linear algebra we just use `span {x}`

.

#### Yury G. Kudryashov (Jul 24 2020 at 19:57):

So we can go with `mem_closure_singleton`

instead of introducing `gpowers`

.

#### Yury G. Kudryashov (Jul 24 2020 at 19:57):

(I don't remember how it is currently done for bundled submonoids and subgroups)

#### Kevin Buzzard (Jul 24 2020 at 21:10):

For bundled submonoids I just added `powers m`

and `multiplies a`

. These things are perhaps much more useful in group theory than ring theory. The subgroup generated by an element is a fundamental construction in the theory of finite groups, but we don't usually analyse vector spaces by drawing lines in them

Last updated: May 12 2021 at 08:14 UTC