proposition: Lemma separable_prod I r (P : pred I) (v_ : I -> L) (K : {subfield L}) : (forall i, P i -> separable_element K (v_ i)) -> separable_element K (\prod_(i <- r | P i) v_ i).
proof: Proof. move=> sepKi. by elim/big_ind: _; [apply/base_separable/mem1v | apply: separable_mulv |]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)