Commit 2023-04-24 05:58 32d4b249

View on Github →

feat: port LinearAlgebra.Matrix.Circulant (#3465)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Circulant.lean

added theorem Matrix.Fin.circulant_inj

added theorem Matrix.Fin.circulant_injective

added theorem Matrix.Fin.circulant_isSymm_apply

added theorem Matrix.Fin.circulant_isSymm_iff

added theorem Matrix.Fin.circulant_ite

added theorem Matrix.Fin.circulant_mul

added theorem Matrix.Fin.circulant_mul_comm

added theorem Matrix.Fin.conjTranspose_circulant

added theorem Matrix.Fin.transpose_circulant

added def Matrix.circulant

added theorem Matrix.circulant_add

added theorem Matrix.circulant_apply

added theorem Matrix.circulant_col_zero_eq

added theorem Matrix.circulant_inj

added theorem Matrix.circulant_injective

added theorem Matrix.circulant_isSymm_apply

added theorem Matrix.circulant_isSymm_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.conjTranspose_circulant

added theorem Matrix.map_circulant

added theorem Matrix.transpose_circulant