delete `mul_right_inv`

Stream: general

[Kevin Buzzard]

There's a function called mul_right_inv in the root namespace, defined in core. I am writing a teaching file where I develop the basics of group theory from scratch, so I have my own definition of group -- a class, in a namespace mygroup. If I make the instance mygroup.group G -> group G then this causes mayhem because I am trying to get my users to prove things like theorem mygroup.group.mul_right_inv (a : G) : a * a⁻¹ = 1 so they can use it later, but if our home-rolled groups are known to be Lean groups then all these theorems are automatically available so the user can apply them in the wrong order to make the API.

My current crappy fix is not to make the instance, so mul_right_inv doesn't actually apply for my groups, but then when the user wants to rewrite it they have to put something like rw group.mul_right_inv (they're always in the mygroup namespace). I can get Lean to complain about an ambiguity in mul_right_inv but I would rather just locally make that function private in my repo so that the user can't possibly be confused about it, because I know it is never what they want to use. Is this possible?

[Sebastian Ullrich]

If you declare that name inside mygroup (abbrev mul_right_inv := @group.mul_right_inv), it will shadow the root declaration instead of overloading it

[Johan Commelin]

Huh, if you don't make the instance, then rw group.mul_right_inv won't work right?

[Johan Commelin]

I'm confused about what your problem is.

[Sebastian Ullrich]

That group is mygroup.group, I assume

[Johan Commelin]

Aha. That makes sense