Commit 2024-04-17 20:41 48970a4b

View on Github →

feat: characteristic polynomials of linear families of endomorphisms (#11773)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/LinearMap/Polynomial.lean

added def LinearMap.polyCharpoly

added def LinearMap.polyCharpolyAux

added theorem LinearMap.polyCharpolyAux_baseChange

added theorem LinearMap.polyCharpolyAux_basisIndep

added theorem LinearMap.polyCharpolyAux_coeff_eval

added theorem LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff

added theorem LinearMap.polyCharpolyAux_map_aeval

added theorem LinearMap.polyCharpolyAux_map_eq_charpoly

added theorem LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly

added theorem LinearMap.polyCharpolyAux_map_eval

added theorem LinearMap.polyCharpoly_baseChange

added theorem LinearMap.polyCharpoly_coeff_eval

added theorem LinearMap.polyCharpoly_coeff_isHomogeneous

added theorem LinearMap.polyCharpoly_coeff_map

added theorem LinearMap.polyCharpoly_eq_of_basis

added theorem LinearMap.polyCharpoly_monic

added theorem LinearMap.polyCharpoly_natDegree

added theorem LinearMap.polyCharpoly_ne_zero

added def LinearMap.toMvPolynomial

added theorem LinearMap.toMvPolynomial_add

added theorem LinearMap.toMvPolynomial_baseChange

added theorem LinearMap.toMvPolynomial_comp

added theorem LinearMap.toMvPolynomial_constantCoeff

added theorem LinearMap.toMvPolynomial_eval_eq_apply

added theorem LinearMap.toMvPolynomial_isHomogeneous

added theorem LinearMap.toMvPolynomial_totalDegree_le

added theorem LinearMap.toMvPolynomial_zero

added def Matrix.toMvPolynomial

added theorem Matrix.toMvPolynomial_add

added theorem Matrix.toMvPolynomial_constantCoeff

added theorem Matrix.toMvPolynomial_eval_eq_apply

added theorem Matrix.toMvPolynomial_isHomogeneous

added theorem Matrix.toMvPolynomial_map

added theorem Matrix.toMvPolynomial_mul

added theorem Matrix.toMvPolynomial_totalDegree_le

added theorem Matrix.toMvPolynomial_zero

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

added theorem MvPolynomial.totalDegree_monomial_le

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

added theorem Basis.end_apply

added theorem Basis.end_apply_apply

added def Basis.linearMap

added theorem Basis.linearMap_apply

added theorem Basis.linearMap_apply_apply

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

modified theorem Algebra.TensorProduct.basis_apply

modified theorem Algebra.TensorProduct.basis_repr_symm_apply'

added theorem Basis.baseChange_end

added theorem Basis.baseChange_linearMap

added def LinearMap.tensorProduct

added def LinearMap.tensorProductEnd