# Zulip Chat Archive

## Stream: maths

### Topic: normalizers

#### Kevin Buzzard (Jul 24 2020 at 08:35):

`subgroup.normalizer`

(src) is the normalizer of a subgoup. This definition works fine for sets too. I changed it to sets, and the same definition still works fine (it never uses that H is a subgroup), but then in the applications I have a gazillion errors because Lean can't figure out the coercion from `subgroup G`

to `set ??`

. Basically, normalizers work for sets, and are occasionally useful for sets, however in pretty much all applications they're used on subgroups. What is the best way to solve this? I'd like to have access to the set normalizer function.

#### Scott Morrison (Jul 24 2020 at 08:38):

Can we write `normalizer`

just in terms of `set`

, and then have a `subgroup.normalizer`

as essentially a forward that that `normalizer`

, that includes the coercion explicitly.

#### Kevin Buzzard (Jul 24 2020 at 08:53):

Which namespace does `normalizer : set G -> subgroup G`

go in? I'm not very good at namespaces

#### Jalex Stark (Jul 24 2020 at 12:09):

`group`

?

#### Jalex Stark (Jul 24 2020 at 12:11):

I'm imagining I've done `open group`

. If I have a set s I can say `normalizer s`

and if I have a subgroup H I can say `H.normalizer`

Last updated: May 19 2021 at 02:10 UTC