Constant matrices

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

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

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

open import foundation.universe-levels

open import linear-algebra.constant-vectors
open import linear-algebra.matrices

Idea

Constant matrices are matrices in which all elements are the same.

Definition

constant-matrix : {l : Level} {A : UU l} {m n : ℕ} → A → matrix A m n
constant-matrix a = constant-vec (constant-vec a)

Recent changes