proposition: Lemma scaleo (F : filter_on T) a (f : T -> V) (e : _ -> W) : a *: [o_F e of f] = [o_F e of a *: [o_F e of f]].
proof: Proof. by rewrite [RHS]littleoE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets functions) ereal reals signed topology normedtype prodnormedzmodule