Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-31 14:15 99e3ffbd

View on Github →

feat(data/fin/tuple): new directory and file on sorting (#11096) Code written by @kmill at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Permutation.20to.20make.20a.20function.20monotone Co-authored by: Kyle Miller kmill31415@gmail.com

Estimated changes

added theorem tuple.graph.card
added def tuple.graph.proj
added def tuple.graph
added theorem tuple.monotone_proj
added theorem tuple.monotone_sort
added theorem tuple.proj_equiv₁'
added theorem tuple.self_comp_sort
added def tuple.sort