List.perm_comm at Data.List.Perm

Stream: mathlib4

[Jihoon Hyun]

Other theorems except perm_comm have naming such as Perm.symm, Perm.swap', etc.. Is this a typo?

[Alex J. Best]

In mathlib we make use of dot notation (where a.b resolves to (type of a).b a) so List.Perm.symm can be used as p.symm. This doesn't work for List.perm_comm as it doesn't have an explicit argument with type Perm, so the name uses an underscore instead to match the usual naming convention.
So you can find many examples of _comm and .symm for different types in mathlib.
As for the capitalization I think this is still a bit in flux so wouldn't want to say that is completely correct