Zulip Chat Archive

Stream: PR reviews

Topic: Signature of a permutation


Antoine Chambert-Loir (Jan 04 2022 at 12:05):

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 (Jan 06 2022 at 12:07):

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


Last updated: Dec 20 2023 at 11:08 UTC