Commit 2024-02-13 12:46 34661a71

View on Github →

chore(LinearAlgebra/Matrix/Charpoly): charpoly of block matrix (#10480)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean

modified theorem Matrix.aeval_self_charpoly

modified def Matrix.charpoly

added theorem Matrix.charpoly_fromBlocks_zero₁₂

added theorem Matrix.charpoly_fromBlocks_zero₂₁

modified theorem Matrix.charpoly_reindex

modified theorem charmatrix_apply

modified theorem charmatrix_apply_eq

modified theorem charmatrix_apply_ne

added theorem charmatrix_fromBlocks

modified theorem charmatrix_reindex

modified theorem matPolyEquiv_charmatrix