agda-stdlib
agda-stdlib copied to clipboard
agda
Some lemmas to do with transposition lists
This is largely preliminaries for #1741, which I'm still playing with how to implement.
I started addressing the comments, but I've been very distracted lately (and have broken my wrist in the meantime). I don't know when I can get back to it
Oh no, sorry to hear that! I can see why that'd make typing a little difficulty. Okay no worries, I'll leave it up and see if I have the time to fiddle with it in the meantime....
Now that #1852 is in, I'd like to continue work on this PR to where I wanted to get it to, proving that there's a group homomorphism from permutations to their parity (this will let us define alternating groups and is useful for implementing Liebniz's formula for matrix determinants)
@Taneb I'm afraid in the end I didn't get a chance to look at it, and no real prospect of it happening soon. Any likelihood of you picking this backup in the next month? Otherwise I propose to close.
It's always been on my to-do list, but I want it to include the parity theorem. Feel free to close it and I'll open a new PR when it's ready
Or you could rebase this PR and then subsequently re-open once you have Parity working...? (sorry we didn't manage to push it over the line last year in Delft!)
