Commit 2024-02-19 08:49 a4fac96e

View on Github →

feat(LinearAlgebra/Charpoly): the characteristic polynomial of a direct sum (#10663) ... is the product of the characteristic polynomials.

Estimated changes

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

added theorem LinearMap.charpoly_natDegree

Modified Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean

added theorem LinearMap.charpoly_prodMap

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

added theorem LinearMap.toMatrix_prodMap