Mathlib.Combinatorics

Finite combinatorial and spectral infrastructure for uniform subset slices and their linear operators.

Johnson­Kneser 16 core · 29 supporting · 3 submodules Johnson harmonic decomposition of uniform subset slices and the Kneser disjointness operator's degree-wise eigenvalues.