proposition: Lemma mleadc_prod_proper : (forall x, x \in r -> P x -> GRing.lreg (mleadc (F x))) -> mleadc (\prod_(p <- r | P p) F p) = \prod_(p <- r | P p) mleadc (F p).
proof: Proof. by move/mlead_prod_proper=> ->; rewrite mleadc_prod. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg