mathlib

Stream: general

[Scott Morrison]

Is it strange that we have monoid.pow and gpow (for groups)? Can we make these more uniform?

[Mario Carneiro]

you mean the names? Do you have a better idea?

[Scott Morrison]

group.pow?

[Mario Carneiro]

eh, I think the reason I didn't do that to begin with is because that puts all the group.pow theorems in the group namespace, which makes stuff longer since it's usually not open.

[Scott Morrison]

I would generally vote for longer over obscure, but I don't have a sense of how bad this would be here.

[Kevin Buzzard]

So why isn't this an argument for mpow, thus not putting all the monoid.pow theorems in the monoid namespace, which is also usually not oen?

[Kenny Lau]

So why isn't this an argument for mpow, thus not putting all the monoid.pow theorems in the monoid namespace, which is also usually not open?

you win

[Mario Carneiro]

you will notice that I only use the monoid namespace when I need to in theorems, as disambiguation

[Mario Carneiro]

but I didn't say the current way is at all consistent, nor am I averse to changing it

[Kevin Buzzard]

I am not suggesting it be changed, I was just being a pedant.