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

open import foundation.universe-levels

open import linear-algebra.vectors

Idea

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

Definition

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