Diagonal vectors

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

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

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

open import foundation.universe-levels

open import linear-algebra.vectors


Diagonal vectors are vectors on the diagonal, i.e., they are vectors of which all coefficients are equal.


constant-vec : {l : Level} {A : UU l} {n : }  A  vec A n
constant-vec {n = zero-ℕ} _ = empty-vec
constant-vec {n = succ-ℕ n} x = x  (constant-vec x)

Recent changes