proposition: Lemma galNorm_prod (I : Type) (r : seq I) (P : pred I) (B : I -> L) : galNorm U V (\prod_(i <- r | P i) B i) = \prod_(i <- r | P i) galNorm U V (B i).
proof: Proof. exact: (big_morph _ galNormM galNorm1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)