Scalar multiplication on matrices

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

Created on 2022-03-16.
Last modified on 2023-03-10.

module linear-algebra.scalar-multiplication-matrices where

open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

open import linear-algebra.matrices
open import linear-algebra.scalar-multiplication-vectors

scalar-mul-matrix :
  {l1 l2 : Level} {B : UU l1} {A : UU l2} {m n : ℕ} →
  (B → A → A) → B → matrix A m n → matrix A m n
scalar-mul-matrix μ = scalar-mul-vec (scalar-mul-vec μ)

Recent changes

• 2023-03-10. Fredrik Bakke. Additions to fix-import (#497).
• 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
• 2023-03-07. Fredrik Bakke. Add blank lines between <details> tags and markdown syntax (#490).
• 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).
• 2023-03-05. Jonathan Prieto-Cubides. Add “suggest an edit” button and minor fix (#484).