mathlib

47b1d786 - feat(linear_algebra/matrix): any matrix power can be expressed as sums of powers `0 ≤ k < fintype.card n` (#12983)

feat(linear_algebra/matrix): any matrix power can be expressed as sums of powers `0 ≤ k < fintype.card n` (#12983) I'm not familiar enough with the polynomial API to know if we can neatly state a similar result for negative powers.