Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-14 01:19 f0a1356c

View on Github →

feat(linear_algebra/matrix/circulant): add a file (#9011)

Estimated changes

Created src/linear_algebra/matrix/circulant.lean

added def matrix.circulant

added theorem matrix.circulant_add

added theorem matrix.circulant_col_zero_eq

added theorem matrix.circulant_inj

added theorem matrix.circulant_injective

added theorem matrix.circulant_is_symm_apply

added theorem matrix.circulant_is_symm_iff

added theorem matrix.circulant_mul

added theorem matrix.circulant_mul_comm

added theorem matrix.circulant_neg

added theorem matrix.circulant_single

added theorem matrix.circulant_single_one

added theorem matrix.circulant_smul

added theorem matrix.circulant_sub

added theorem matrix.circulant_zero

added theorem matrix.conj_transpose_circulant

added theorem matrix.fin.circulant_inj

added theorem matrix.fin.circulant_injective

added theorem matrix.fin.circulant_is_symm_apply

added theorem matrix.fin.circulant_is_symm_iff

added theorem matrix.fin.circulant_ite

added theorem matrix.fin.circulant_mul

added theorem matrix.fin.circulant_mul_comm

added theorem matrix.fin.conj_transpose_circulant

added theorem matrix.fin.transpose_circulant

added theorem matrix.map_circulant

added theorem matrix.transpose_circulant