Signature of a permutation

Stream: PR reviews

[Antoine Chambert-Loir]

I have made a small PR #11233 where I compute the signature of a permutation from its cycle type. The formula is simpler than doc#sign_of_cycle_type. branch#sign_from_cycle_type' .

I have two proofs. The one here in the PR makes use of doc#sign_of_cycle_type.
I have another one, direct, which might be the one to add to mathlib if doc#sign_of_cycle_type is only rarely used.

[Antoine Chambert-Loir]

Since I couldn't have VSCode compile on that branch, I closed this PR and opened a new one, that works.
#11281