Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.fin.conj_transpose_circulant

Modification history

2021-09-14 01:19
src/linear_algebra/matrix/circulant.lean
feat(linear_algebra/matrix/circulant): add a file (#9011)
Added matrix.fin.conj_transpose_circulantView on Github →