Theorems · Definition · linear algebra

Matrix.circulant

{α : Type u_1} → {n : Type u_3} → [Sub n] → (n → α) → Matrix n n α

Given the condition [Sub n] and a vector v : n → α, we define circulant v to be the circulant matrix generated by v of type Matrix n n α. The (i,j)th entry is defined to be v (i - j).

Defined in

Mathlib.LinearAlgebra.Matrix.Circulant

Cited by

27 results in Mathlib

Foundations

Depth 14 from the axioms · uses Quot.sound

Assumes

Sub