proposition: Theorem prime_dim_normed_finField : (p <= q)%N.
proof: Proof. apply: wlog_neg; rewrite -ltnNge => ltqp. have [F sigma /isomP[inj_sigma im_sigma] defP0] := fieldH. case=> sigmaU inj_sigmaU sigmaJ. have oF: #|F| = (p ^ q)%N by rewrite -cardsT -im_sigma card_injm. have charFp: p \in [char F] := card_finCharP oF pr_p. have sP0P: P0 \subset P by rewrite -defP0 subsetIl. pose s := invm inj_sigma 1%R. have sigma_s: sigma s = 1%R by rewrite invmK ?im_sigma ?inE. have{} defP0: <[s]> = P0. by rewrite -morphim_cycle /= ?im_sigma ?inE // morphim_invmE. exact: BGappendixC_inner_subproof defP0 sigmaJ. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype choice ssrnat seq div fintype tuple finfun) mathcomp(bigop order ssralg finset prime binomial poly polydiv) mathcomp(fingroup morphism quotient automorphism action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator pgroup abelian frobenius) odd_order(BGsection1) mathcomp(matrix mxalgebra mxabelem vector falgebra fieldext galois) mathcomp(finfield ssrnum algC classfun character integral_char inertia)