def mkVectorSpace {K : Type u_3} {X : Type u_4} [Field K] [AddCommGroup X] (ρ : K →+* AddMonoid.End X) : Module K X

Equations

• mkVectorSpace ρ = Module.mk ⋯ ⋯