Scalar multiplication of tuples

Content created by Louis Wasserman.

Created on 2025-05-14.
Last modified on 2025-05-14.

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

open import foundation.universe-levels

open import lists.functoriality-tuples
open import lists.tuples

Idea

Any operation B → A → A for some type B of formal scalars induces an operation on tuples B → tuple n A → tuple n A.

Definition

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

Recent changes