Commit 2025-03-11 10:17 612ede9f

View on Github →

chore(RingTheory/PolynomialAlgebra): split (#22814) This moves the Matrix / Polynomial interaction to a new file.

Estimated changes

Modified Mathlib.lean

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

Created Mathlib/RingTheory/MatrixPolynomialAlgebra.lean

added def RingHom.polyToMatrix

added theorem evalRingHom_mapMatrix_comp_compRingEquiv

added theorem evalRingHom_mapMatrix_comp_polyToMatrix

added theorem matPolyEquiv_coeff_apply

added theorem matPolyEquiv_coeff_apply_aux_1

added theorem matPolyEquiv_coeff_apply_aux_2

added theorem matPolyEquiv_diagonal_X

added theorem matPolyEquiv_map_C

added theorem matPolyEquiv_map_smul

added theorem matPolyEquiv_smul_one

added theorem matPolyEquiv_symm_C

added theorem matPolyEquiv_symm_X

added theorem matPolyEquiv_symm_apply_coeff

added theorem support_subset_support_matPolyEquiv

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

deleted def RingHom.polyToMatrix

deleted theorem evalRingHom_mapMatrix_comp_compRingEquiv

deleted theorem evalRingHom_mapMatrix_comp_polyToMatrix

deleted theorem matPolyEquiv_coeff_apply

deleted theorem matPolyEquiv_coeff_apply_aux_1

deleted theorem matPolyEquiv_coeff_apply_aux_2

deleted theorem matPolyEquiv_diagonal_X

deleted theorem matPolyEquiv_map_C

deleted theorem matPolyEquiv_map_smul

deleted theorem matPolyEquiv_smul_one

deleted theorem matPolyEquiv_symm_C

deleted theorem matPolyEquiv_symm_X

deleted theorem matPolyEquiv_symm_apply_coeff

deleted theorem support_subset_support_matPolyEquiv

Modified scripts/noshake.json