Constant matrices

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

Created on 2022-03-22.
Last modified on 2025-05-14.

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

open import foundation.universe-levels

open import linear-algebra.constant-tuples
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-tuple (constant-tuple a)

Recent changes