OAI/NumberTheory/Catalan/Determinants/PalindromicOriginalDeterminantFactorization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.palindromicReducedBlockMatrix_conjugate line 13
2. theorem OAI.InternalCatalan.palindromicEigenBlock_eq_reindexed_blockDiagonal line 24
3. theorem OAI.InternalCatalan.det_palindromicReducedBlockMatrix_eq_product line 38
4. theorem OAI.InternalCatalan.det_palindromicReducedBlockMatrix_factorization line 67
5. theorem OAI.InternalCatalan.det_palindromicResidueBlockMatrix_factorization line 78
6. theorem OAI.InternalCatalan.det_palindromicScaledResidueMatrix_factorization line 98
7. theorem OAI.InternalCatalan.palindromic_original_determinant_residue_factorization line 108