proposition: Theorem finDomain_mulrC : @commutative R R *%R.
proof: Proof. have fieldR := finDomain_field. have [p p_pr charRp]: exists2 p, prime p & p \in [char R]. have [e /prod_prime_decomp->]: {e | (e > 0)%N & e%:R == 0 :> R}. by exists #|[set: R]%G|; rewrite // -order_dvdn order_dvdG ?inE. rewrite big_seq; elim/big_rec: _ => [|[p m] /= n]; first by rewrite oner_eq0. case/mem_prime_decomp=> p_pr _ _ IHn. elim: m => [|m IHm]; rewrite ?mul1n {IHn}// expnS -mulnA natrM. by case/eqP/domR/orP=> //; exists p; last apply/andP. pose Rp := PrimeCharType charRp; pose L : {vspace Rp} := fullv. pose G := [set: {unit R}]; pose ofG : {unit R} -> Rp := val. pose projG (E : {vspace Rp}) := [preim ofG of E]. have inG t nzt: Sub t (finDomain_field nzt) \in G by rewrite inE. have card_projG E: #|projG E| = (p ^ \dim E - 1)%N. transitivity #|E|.-1; last by rewrite subn1 card_vspace card_Fp. rewrite (cardD1 0) mem0v (card_preim val_inj) /=. apply: eq_card => x; congr (_ && _); rewrite [LHS]codom_val. by apply/idP/idP=> [/(memPn _ _)-> | /fieldR]; rewrite ?unitr0. pose C u := 'C[ofG u]%AS; pose Q := 'C(L)%AS; pose q := (p ^ \dim Q)%N. have defC u: 'C[u] =i projG (C u). by move=> v; rewrite cent1E !inE (sameP cent1vP eqP). have defQ: 'Z(G) =i projG Q. move=> u /[!inE]. apply/centP/centvP=> cGu v _; last exact/val_inj/cGu/memvf. by have [-> | /inG/cGu[]] := eqVneq v 0; first by rewrite commr0. have q_gt1: (1 < q)%N by rewrite (ltn_exp2l 0) ?prime_gt1 ?adim_gt0. pose n := \dim_Q L; have oG: #|G| = (q ^ n - 1)%N. rewrite -expnM mulnC divnK ?skew_field_dimS ?subvf // -card_projG. by apply: eq_card => u; rewrite !inE memvf. have oZ: #|'Z(G)| = (q - 1)%N by rewrite -card_projG; apply: eq_card. suffices n_le1: (n <= 1)%N. move=> u v; apply/centvsP: (memvf (u : Rp)) (memvf (v : Rp)) => {u v}. rewrite -(geq_leqif (dimv_leqif_sup (subvf Q))) -/L. by rewrite leq_divLR ?mul1n ?skew_field_dimS ?subvf in n_le1. without loss n_gt1: / (1 < n)%N by rewrite ltnNge; apply: wlog_neg. have [q_gt0 n_gt0] := (ltnW q_gt1, ltnW n_gt1). have [z z_prim] := C_prim_root_exists n_gt0. have zn1: z ^+ n = 1 by apply: prim_expr_order. have /eqP-n1z: `|z| == 1 by rewrite -(pexpr_eq1 n_gt0) // -normrX zn1 normr1. suffices /eqP/normCBeq[t n1t [Dq Dz]]: `|q%:R - z : algC| == `|q%:R : algC| - `|z|. suffices z1: z == 1 by rewrite leq_eqVlt -dvdn1 (prim_order_dvd z_prim) z1. by rewrite Dz n1z mul1r -(eqr_pMn2r q_gt0) Dq normr_nat mulr_natl. pose aq d : algC := (cyclotomic (z ^+ (n %/ d)) d).[q%:R]. suffices: `|aq n| <= (q - 1)%:R. rewrite eq_le lerB_dist andbT n1z normr_nat natrB //; apply: le_trans. rewrite {}/aq horner_prod divnn n_gt0 expr1 normr_prod. rewrite (bigD1 (Ordinal n_gt1)) ?coprime1n //= !hornerE ler_peMr //. elim/big_ind: _ => // [|d _]; first exact: mulr_ege1. rewrite !hornerE; apply: le_trans (lerB_dist _ _). by rewrite normr_nat normrX n1z expr1n lerBDl (leC_nat 2). have Zaq d: d %| n -> aq d \in Num.int. move/(dvdn_prim_root z_prim)=> zd_prim. rewrite rpred_horner ?rpred_nat //= -Cintr_Cyclotomic //. by apply/polyOverP=> i; rewrite coef_map ?rpred_int. suffices: (aq n %| (q - 1)%:R)%C. rewrite {1}[aq n]intrEsign ?Zaq // -(rpredMsign _ (aq n < 0)%R). rewrite dvdC_mul2l ?signr_eq0 //. have /natrP[m ->]: `|aq n| \in Num.nat by rewrite natr_norm_int ?Zaq. by rewrite leC_nat dvdC_nat; apply: dvdn_leq; rewrite subn_gt0. have prod_aq m: m %| n -> \prod_(d < n.+1 | d %| m) aq d = (q ^ m - 1)%:R. move=> m_dv_n; transitivity ('X^m - 1).[q%:R : algC]; last first. by rewrite !hornerE -natrX natrB ?expn_gt0 ?prime_gt0. rewrite (prod_cyclotomic (dvdn_prim_root z_prim m_dv_n)). have def_divm: perm_eq (divisors m) [seq d <- index_iota 0 n.+1 | d %| m]. rewrite uniq_perm ?divisors_uniq ?filter_uniq ?iota_uniq // => d. rewrite -dvdn_divisors ?(dvdn_gt0 n_gt0) // mem_filter mem_iota ltnS /=. by apply/esym/andb_idr=> d_dv_m; rewrite dvdn_leq ?(dvdn_trans d_dv_m). rewrite (perm_big _ def_divm) big_filter big_mkord horner_prod. by apply: eq_bigr => d d_dv_m; rewrite -exprM muln_divA ?divnK. have /rpredBl<-: (aq n %| #|G|%:R)%C. rewrite oG -prod_aq // (bigD1 ord_max) //= dvdC_mulr //. by apply: rpred_prod => d /andP[/Zaq]. rewrite center_class_formula addrC oZ natrD addKr natr_sum /=. apply: rpred_sum => _ /imsetP[u /setDP[_ Z'u] ->]; rewrite -/G /=. have sQC: (Q <= C u)%VS by apply/subvP=> v /centvP-cLv; apply/cent1vP/cLv/memvf. have{sQC} /dvdnP[m Dm]: \dim Q %| \dim (C u) by apply: skew_field_dimS. have m_dv_n: m %| n by rewrite dvdn_divRL // -?Dm ?skew_field_dimS ?subvf. have m_gt0: (0 < m)%N := dvdn_gt0 n_gt0 m_dv_n. have{Dm} oCu: #|'C[u]| = (q ^ m - 1)%N. by rewrite -expnM mulnC -Dm (eq_card (defC u)) card_projG. have ->: #|u ^: G|%:R = \prod_(d < n.+1 | d %| n) (aq d / aq d ^+ (d %| m)). rewrite -index_cent1 natf_indexg ?subsetT //= setTI prodf_div prod_aq // -oG. congr (_ / _); rewrite big_mkcond oCu -prod_aq //= big_mkcond /=. by apply: eq_bigr => d _; case: ifP => [/dvdn_trans->| _]; rewrite ?if_same. rewrite (bigD1 ord_max) //= [n %| m](contraNF _ Z'u) => [|n_dv_m]; last first. rewrite -sub_cent1 subEproper eq_sym eqEcard subsetT oG oCu leq_sub2r //. by rewrite leq_exp2l // dvdn_leq. rewrite divr1 dvdC_mulr //; apply/rpred_prod => d /andP[/Zaq-Zaqd _]. have [-> | nz_aqd] := eqVneq (aq d) 0; first by rewrite mul0r /=. by rewrite -[aq d]expr1 -exprB ?leq_b1 ?unitfE ?rpredX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype div tuple bigop prime finset fingroup) mathcomp(ssralg poly polydiv morphism action countalg) mathcomp(finalg zmodp cyclic center pgroup abelian matrix) mathcomp(mxpoly vector falgebra fieldext separable galois)