Theorem Module.finrank_baseChange

Modification history

2024-11-13 09:53
Mathlib/LinearAlgebra/Dimension/Constructions.lean
feat(LinearAlgebra): charpoly of base-change of linear map (#18423)
Added Module.finrank_baseChangeView on Github →