Commit 2024-11-13 09:53 b3693833

View on Github →

feat(LinearAlgebra): charpoly of base-change of linear map (#18423)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Charpoly/BaseChange.lean

added theorem LinearMap.charpoly_baseChange

added theorem LinearMap.det_baseChange

added theorem LinearMap.det_eq_sign_charpoly_coeff

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

added theorem Module.finrank_baseChange

added theorem Module.rank_baseChange