**Coq-Combi - Algebraic combinatorics in Coq**
*Date of the last release: 26 October 2015*
Person in charge :

HIVERT Florent
- the Littlewood-Richardson rule using Schützeberger approach, it includes

the Robinson-Schensted correspondance

the construction of the plactic monoïd

the Littlewood-Richardson and Pieri rules using the combinatorial (tableau definition of Schur polynomials).

- basic theory of symmetric functions including

Schur function and Kostka numbers and the equivalence of the combinatorial and algebraic (Jacobi) definition of Schur functions

the classical bases, Newton formulas and various basis changes

the scalar product and the Cauchy formula.

- the character theory of the symmetric Groups. We do not use representations but rather goes as fast as possible to Frobenius isomorphism and then uses computations with symmetric polynomials. it includes

cycle types for permutations (together with Thibaut Benjamin)

The tower structure and the restriction and induction formulas for class indicator (together with Thibaut Benjamin)

structure of the centralizer of a permutation

Young character and Young Rule

the theory of Frobenius characteristic and Frobenius character formula

the Littlewood-Richardson rule for irreducible character

- the Hook-Length Formula for standard Young tableaux (together with Christine Paulin and Olivier Stietel)

- the Erdös Szekeres theorem about increassing and decreassing subsequences

- various Combinatorial objects including

totally and partially ordered types,

integer partitions and compositions,

tableaux, standard tableaux, skew tableaux,

subsequences, integer vectors,

standard words and permutations,

Yamanouchi words

- the Coxeter presentation of the symmetric group.

- the factorization of the Vandermonde determinant as the product of differences.

*More information: *https://github.com/hivert/Coq-Combi
Software

**Research activities**
**Members**
HIVERT Florent
**Group**