# Zulip Chat Archive

## Stream: new members

### Topic: (topological) quotient group

#### Daan van Gent (Jul 18 2020 at 16:07):

I am trying to define the topological group \R / \Z and I am running into some problems. First one has to construct the subgroup \Z of \R. Apparently this can be done in two ways, with `add_subgroup`

and `is_add_subgroup`

. The latter is deprecated, but the former has no quotient definition associated as far as I know. What should I do?

#### Heather Macbeth (Jul 18 2020 at 16:28):

The experts will answer you soon, but the short answer is that you have found a refactor-in-progress. #3321

#### Kevin Buzzard (Jul 18 2020 at 16:48):

I just got `quotient_group.lean`

compiling with `add_subgroup`

and no errors an hour ago :-)

#### Alex J. Best (Jul 18 2020 at 17:12):

Maybe you are doing this already but I'd recommend explcitly defining Z inside R as the image of the coercion map from Z to R. You might get more results for free that way

#### Kevin Buzzard (Jul 18 2020 at 17:21):

Before `norm_cast`

I was considering making two typeclasses on `real`

, both called something like `is_int`

, one a predicate ("there exists an integer such that I'm the coercion of that integer") and one containing data (the integer plus a proof that the integer coerces to the real in question). Type class inference could be used to show that the sum of two real integers was a real integer etc

#### Daan van Gent (Jul 18 2020 at 18:08):

Alex J. Best said:

Maybe you are doing this already but I'd recommend explcitly defining Z inside R as the image of the coercion map from Z to R. You might get more results for free that way

I define Z as the subgroup generated by 1 in R. I'll see whether your suggestion turns out to be more useful when I get to working with it.

#### Daan van Gent (Jul 18 2020 at 18:09):

Thanks for your answers. I guess I'll wait a bit before playing around with groups some more.

Last updated: Dec 20 2023 at 11:08 UTC