Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import 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.