Scalar multiplication of vectors

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-03-15.
Last modified on 2023-03-13.

module linear-algebra.scalar-multiplication-vectors where
open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

open import linear-algebra.functoriality-vectors
open import linear-algebra.vectors


Any operation B → A → A for some type B of formal scalars induces an operation B → vec n A → vec n A.


scalar-mul-vec :
  {l1 l2 : Level} {B : UU l1} {A : UU l2} {n : } 
  (B  A  A)  B  vec A n  vec A n
scalar-mul-vec μ x = map-vec (μ x)

Recent changes