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
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

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

Idea

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

Definition

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