proposition: Fact baseField_scaleA a b u : a *F0: (b *F0: u) = (a * b) *F0: u.
proof: Proof. by rewrite [_ *F0: _]scalerA -rmorphM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)