proposition: Theorem Frobenius_ident : n`! = \sum_(p : 'P_n) (n`! %/ (hook_length_prod p))^2.
proof: Proof. Proof using. rewrite -{1}card_stdwordn -card_stpn_shape_hook. have rst1 (w : stdwordn n) : is_stdtab_of_n n (RStabmap w).1. by rewrite RStabmapE /= RSstdE stdwordnP /= size_RS size_sdtn. have rst2 (w : stdwordn n) : is_stdtab_of_n n (RStabmap w).2. rewrite /= is_stdtab_RStabmap2 /size_tab -shape_RStabmapE. by rewrite RStabmapE -/(size_tab _) size_RS size_sdtn eqxx. pose to_pair (w : stdwordn n) := (StdtabN (rst1 w), StdtabN (rst2 w)). pose stdrspair (p : stpn) := if shape p.1 == shape p.2 then (val p.1, val p.2) else (val p.1, val p.1) . have stdrspairP p : is_RStabpair (stdrspair p). rewrite /is_RStabpair/stdrspair. by case: eqP => /= [-> |_]; rewrite stdtabnP eqxx stdtabP. pose stdrsinv p := RStabinv (RSTabPair (stdrspairP p)). have from_pairP p : is_std_of_n n (stdrsinv p). case: p => [t1 t2]; rewrite /= /stdrsinv /= -RSstdE -size_RS -RStabmapE. rewrite -[RStabmap _]/(val (RStab _)) RStabinvK /stdrspair /=. rewrite [(_).1](_ : _ = val t1); last by case eqP. by rewrite stdtabnP /= size_tab_stdtabn. pose from_pair p := StdWordN (from_pairP p). have to_pairK : cancel to_pair from_pair. move=> w; apply val_inj; rewrite /= /stdrsinv /= /stdrspair /to_pair. rewrite [RSTabPair _](_ : _ = RStab w) ?RStabK //. apply val_inj; rewrite /= /stdrspair /= shape_RStabmapE eqxx. by case: RStabmap. rewrite -(card_imset _ (can_inj to_pairK)); apply eq_card => [[/= t1 t2]]. rewrite inE /=; apply/imsetP/idP => /= [[w _ [->{t1} ->{t2}/=]] | eqsh]. by rewrite shape_RStabmapE. exists (from_pair (t1, t2)); first by []. apply/eqP; rewrite xpair_eqE /= -!val_eqE /= /stdrsinv. by rewrite -[RStabmap _]/(val (RStab _)) RStabinvK /= /stdrspair eqsh !eqxx. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype choice ssrnat seq ssrint div rat fintype finset bigop path ssralg ssrnum order) ordtype partition tableau Schensted std stdtab hook