[Merged by Bors] - feat(data/equiv/derangements/basic): define derangements #7526

HenrySwanson · 2021-05-06T02:29:40Z

This proves two formulas for the number of derangements on n elements, and defines some combinatorial equivalences
involving derangements on α and derangements on certain subsets of α. This proves Theorem 88 on Freek's list.

This is rather messy; would really appreciate suggestions. I read through a few mathlib files, but I'm definitely not
super-familiar with Lean conventions yet.

I have a bunch of specific things I'd like feedback on, with -- TODO comments.

I'm also trying to get something with equiv.perm.decompose_option working, but it's not looking promising. :| There's a nice equivalence from perm (option α) to (option α) x (perm α) that could be used. It restricts on derangements to α x {f : perm α // [no fixed points, or f(none) is the only fixed point]}, which is tempting, for obvious reasons. But the intermediate casting of subtypes is hard. I'll update this if it works out, but it's not looking like it'll be any cleaner.

This is rather messy; would really appreciate suggestions. I read through a few mathlib files, but I'm definitely not super-familiar with Lean conventions yet.

oops, left the wrong name in after copy-pasting

archive/100-theorems-list/88_derangements_formula.lean

Ruben-VandeVelde

Some stylistic suggestions:

archive/100-theorems-list/88_derangements_formula.lean

HenrySwanson · 2021-05-07T03:21:50Z

FWIW i did manage to get the option-based approach working last night: https://pastebin.com/aCKb5TqW

i don't know if one way or the other is more lean-y, but i'm happy to submit whichever one makes more sense

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>

archive/100-theorems-list/88_derangements_formula.lean

It turns out that working with `derangements (option \alpha)` was much easier, mostly because working with `\alpha` is easier than working with the set `{a}^c` for some `a`. So this got around a lot of the issues with sets/types and giving things names to appease the elaborator. There's still a few more TODOs, but I've incorporated the changes that were suggested (e.g. no non-terminal simps, style guidelines, pull things into files).

src/data/equiv/derangements/basic.lean

YaelDillies

This is looking good!

Here's my final batch of suggestions. LGTM otherwise

src/combinatorics/derangements/basic.lean

src/data/equiv/basic.lean

src/combinatorics/derangements/basic.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/combinatorics/derangements/basic.lean

semorrison · 2021-09-07T00:02:08Z

@HenrySwanson, there are a bunch of "outdated" but "unresolved" conversations above. Could you please clean those up (either explaining why they are still unresolved, or just clicking resolve), so I can easily tell where things stand?

HenrySwanson · 2021-09-07T01:18:05Z

@semorrison Okay, I've been able to resolve all but one of them. Once that last one is done I can ping you on Zulip :)

src/combinatorics/derangements/basic.lean

semorrison · 2021-09-08T03:48:55Z

bors d+

bors · 2021-09-08T03:48:56Z

✌️ HenrySwanson can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

HenrySwanson · 2021-09-08T07:48:38Z

bors r+

This proves two formulas for the number of derangements on _n_ elements, and defines some combinatorial equivalences involving derangements on α and derangements on certain subsets of α. This proves Theorem 88 on Freek's list. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

bors · 2021-09-08T10:25:26Z

Pull request successfully merged into master.

Build succeeded:

Also, added entries back to 100.yaml

…ments (#9089) This defines `card_derangements` as the cardinality of the set of derangements of a fintype, and `num_derangements` as a function from N to N, and proves their equality, along with some other lemmas. Context: PR #7526 grew too large and had to be split in half. The first half retained the original PR ID, and this is the second half. This adds back the finite.lean and exponential.lean files. Also, added entries back to 100.yaml. Co-authored-by: Johan Commelin <johan@commelin.net>

feat(archive/100-theorems-list): add proof of derangement formula

be28cf1

This is rather messy; would really appreciate suggestions. I read through a few mathlib files, but I'm definitely not super-familiar with Lean conventions yet.

HenrySwanson added the awaiting-review The author would like community review of the PR label May 6, 2021

Fix header message, and update 100.yaml

3f98d10

oops, left the wrong name in after copy-pasting

semorrison reviewed May 6, 2021

View reviewed changes