Diagonal tuples

Content created by Louis Wasserman.

Created on 2025-05-14.
Last modified on 2025-05-14.

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

open import foundation.universe-levels

open import lists.tuples

Idea

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

Definition

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

Recent changes