group namespace

Stream: maths

[Chris Hughes]

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]

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

[Chris Hughes]

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]

where are we using the group namespace?

[Mario Carneiro]

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

[Chris Hughes]

I was using conjugates_of_set which is in the group namespace.

[Koundinya Vajjha]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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