Stream: maths

Topic: group namespace

Chris Hughes (May 31 2019 at 16:11):

Should we not use the group namespace?

namespace group

example {α : Type*} [group α] (a b c : α) : a * b * c = a * (b * c) :=
begin
simp [mul_assoc], -- ⊢ mul a (mul b c) = a * (b * c)
end


The trouble is it used group.mul_assoc instead of mul_assoc, so we ended up with group.mul in the goal

Mario Carneiro (May 31 2019 at 16:26):

you could use _root_.mul_assoc, or you could not be in the namespace but declare the theorem as theorem group.foo ...

Chris Hughes (May 31 2019 at 16:29):

I know, but last time this came up it took me ages to work out what was going on. Which makes things hard for people who don't know the tricks.

Mario Carneiro (May 31 2019 at 16:37):

where are we using the group namespace?

Mario Carneiro (May 31 2019 at 16:38):

Actually I think opening lots of namespaces is something I see a lot but don't really recommend

Chris Hughes (May 31 2019 at 16:46):

I was using conjugates_of_set which is in the group namespace.

Koundinya Vajjha (May 31 2019 at 17:44):

I face this issue with the integration library as well. Some results are nested within two namespaces, and I have to type out the whole thing to access them..

Mario Carneiro (May 31 2019 at 17:49):

the open command is really powerful, you should try some of the options

Johan Commelin (May 31 2019 at 18:02):

Another (currently unavailable) solution would be if we could make group.mul_assoc protected or hidden or whatever.

Johan Commelin (May 31 2019 at 18:03):

Maybe structure fields should be protected by default. Is this a reasonable feature request for 3.?.c?

Mario Carneiro (May 31 2019 at 18:06):

I don't know... that sounds like it will break peoples' things

Mario Carneiro (May 31 2019 at 18:07):

unless we give them an alternative I don't think that's reasonable

Last updated: May 11 2021 at 15:12 UTC