proposition: Lemma char0_ratr_prod I r (P : pred I) E : ratrL (\prod_(i <- r | P i) E i) = \prod_(i <- r | P i) ratrL (E i).
proof: Proof. exact: rmorph_prod. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra all_field)