RFC: Standardise naming for instances

[kckennylau]

Currently, we have 300+ instances with a manual name like instance instCommGroup : CommGroup _, and 700+ instances with a manual name that does not contain inst.

I think not having a standardised policy for these names can create confusion, so I urge the community to decide on one standard for the future.

Arguments for inst:

• Kenny (the author) thinks that this is more consistent with the automatically generated names, which reduces the burden on the user when trying to guess the name, as it is inefficient to first try Rat.commRing and then Rat.instCommRing.

Arguments against inst:

• Andrew Yang thinks that the automatically generated names are intentionally different to discourage people from mentioning them.

There also seem to be people with the opinion that we should not have explicit instance names at all, which is also one possible option.

Zulip: mathlib4 > naming convention: "inst" in instance names