Theorem LinearMap.det_eq_sign_charpoly_coeff

Modification history

2025-11-16 15:54
Mathlib/LinearAlgebra/Charpoly/BaseChange.lean
feat(LinearAlgebra/SpecialLinearGroup): special linear group of a module (#30987) …
Modified LinearMap.det_eq_sign_charpoly_coeffView on Github →
2024-11-13 09:53
Mathlib/LinearAlgebra/Charpoly/BaseChange.lean
feat(LinearAlgebra): charpoly of base-change of linear map (#18423)
Added LinearMap.det_eq_sign_charpoly_coeffView on Github →