normalizers

Stream: maths

[Kevin Buzzard]

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]

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]

Which namespace does normalizer : set G -> subgroup G go in? I'm not very good at namespaces

[Jalex Stark]

group?

[Jalex Stark]

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