From Corelib Require Import Setoid.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq
        ssrint div rat fintype finset bigop path ssralg ssrnum order.

Set Implicit Arguments.

Require Import ordtype partition tableau Schensted std stdtab hook.

Section Identity.

Variable n : nat.

#[local] Notation stpn := (stdtabn n * stdtabn n)%type.
Lemma card_stpn_shape :
  #|[set p : stpn | shape p.1 == shape p.2]| =
    \sum_(sh : 'P_n) #|{: stdtabsh sh}|^2.

Lemma card_stpn_shape_hook :
  #|[set p : stpn | shape p.1 == shape p.2]| =
    \sum_(sh : 'P_n) (n`! %/ (hook_length_prod sh))^2.

Theorem Frobenius_ident :
  n`! = \sum_(p : 'P_n) (n`! %/ (hook_length_prod p))^2.

#[local] Open Scope ring_scope.

Import GRing.Theory.
Import Num.Theory.

Theorem Frobenius_ident_rat :
  1 / (n`!)%:Q = \sum_(p : 'P_n) 1 / (hook_length_prod p)%:Q ^+ 2.

End Identity.