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

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

• 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).