Commit 2024-02-14 03:21 72068a15

View on Github →

feat(LinearAlgebra/Charpoly): the universal characteristic polynomial (#10358)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/MvPolynomial/Basic.lean

Modified Mathlib/Data/MvPolynomial/Equiv.lean

added theorem MvPolynomial.finSuccEquiv_rename_finSuccEquiv

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

added theorem Matrix.charpoly_map

added theorem charmatrix_map

Created Mathlib/LinearAlgebra/Matrix/Charpoly/Univ.lean

added theorem Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous

added theorem Matrix.charpoly.univ_coeff_card

added theorem Matrix.charpoly.univ_coeff_eval₂Hom

added theorem Matrix.charpoly.univ_coeff_isHomogeneous

added theorem Matrix.charpoly.univ_map_eval₂Hom

added theorem Matrix.charpoly.univ_map_map

added theorem Matrix.charpoly.univ_monic

added theorem Matrix.charpoly.univ_natDegree

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

added theorem MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm