Theorem charmatrix_apply_natDegree_le

Modification history

2024-02-15 16:15
Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
chore(LinearAlgebra/Matrix/Charpoly): place more decls in Matrix namespace (#10488)
Deleted charmatrix_apply_natDegree_leView on Github →
2023-05-29 10:13
Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
chore: tidy various files (#4466)
Modified charmatrix_apply_natDegree_leView on Github →
2023-05-21 17:21
Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
feat: port LinearAlgebra.Matrix.Charpoly.Coeff (#4169) …
Added charmatrix_apply_natDegree_leView on Github →