Naming smul vs sMul

Stream: mathlib4

[Richard Osborn]

Not that it is incredibly important but I am currently working on porting GroupTheory.GroupAction.Units and noticed that SMul.smul is named differently that similar classes such as HMul.hMul. Should this be fixed or are people happier with smul?

[Floris van Doorn]

I guess smul should be sMul to be consistent with hMul. I like smul better, but I don't know if that is good enough for an exception to the naming conventions: https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#naming-convention

[Richard Osborn]

Yea, part of the reason I asked is that I also like the look of smul.
There might be one problem with using smul in that it is not clear when to use SMul as lowerCamelCase within a name or to use smul. The issue is avoided with SMul and sMul being the same in lowerCamelCase.

[Richard Osborn]

Ultimately, sMul itself is generally hidden behind notation, so it’s primarily a matter or how it looks within theorems

[Jireh Loreaux]

I think you might be able to argue this falls under Acronyms like LE are written upper-/lowercase as a group, depending on what the first character would be, which would imply smul is the correct form.

[Scott Morrison]

I like smul more.

[Mario Carneiro]

yes, part of the reason for that clause in the naming convention is to allow smul as the lowercased version of SMul