Commit 2024-02-15 16:15 9f7fef49

View on Github →

chore(LinearAlgebra/Matrix/Charpoly): place more decls in Matrix namespace (#10488)

Estimated changes

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

added def Matrix.charmatrix

added theorem Matrix.charmatrix_apply

added theorem Matrix.charmatrix_apply_eq

added theorem Matrix.charmatrix_apply_ne

added theorem Matrix.charmatrix_fromBlocks

added theorem Matrix.charmatrix_map

added theorem Matrix.charmatrix_reindex

added theorem Matrix.matPolyEquiv_charmatrix

deleted def charmatrix

deleted theorem charmatrix_apply

deleted theorem charmatrix_apply_eq

deleted theorem charmatrix_apply_ne

deleted theorem charmatrix_fromBlocks

deleted theorem charmatrix_map

deleted theorem charmatrix_reindex

deleted theorem matPolyEquiv_charmatrix

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

added theorem Matrix.charmatrix_apply_natDegree

added theorem Matrix.charmatrix_apply_natDegree_le

added theorem Matrix.coeff_charpoly_mem_ideal_pow

deleted theorem charmatrix_apply_natDegree

deleted theorem charmatrix_apply_natDegree_le

deleted theorem coeff_charpoly_mem_ideal_pow

added theorem matPolyEquiv_eq_X_pow_sub_C

deleted theorem matPolyEquiv_eq_x_pow_sub_c

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