# Zulip Chat Archive

## Stream: new members

### Topic: Vector space over continuous functions

#### Nicolò Cavalleri (Jul 11 2020 at 14:22):

Oh ok I think I know an example of what you are talking about: it looks type class inference does not work very well for `is_subring`

in the instance `continuous_ring`

#### Nicolò Cavalleri (Jul 11 2020 at 14:25):

In any case I guess then the file `continuous_functions`

will be changed with definitions of subgroups instead of `is_subgroup`

and all of this will be done over continuous bundled functions instead of the subtype of continuous functions as @Scott Morrison was suggesting

#### Nicolò Cavalleri (Jul 11 2020 at 14:25):

If I have time I can try to do it at some point

#### Nicolò Cavalleri (Jul 11 2020 at 14:27):

But for example it seems that the structure `subring`

is not there yet so it's too early to do that

#### Alex J. Best (Jul 11 2020 at 14:32):

Theres also the possibility to use the theory of lattices with `subgroup`

, we can set up an order on subgroups by containment (so far just like sets), and then take things like the least upper bound of two subgroups, which is the smallest subgroup containing both (the subgroup generated by their union rather than just taking the union as sets). I think that sort of thing was harder to arrange with `is_subgroup`

.

#### Kevin Buzzard (Jul 11 2020 at 14:33):

`subgroup G`

has a lattice structure, but the `sup`

is not the one induced from `sup`

on `set G`

, as the union of two subgroups is typically not a subgroup.

Last updated: May 14 2021 at 12:18 UTC