mathlib

c0dbe14d - feat(linear_algebra/matrix/fpow): integer powers of matrices (#8683)

feat(linear_algebra/matrix/fpow): integer powers of matrices (#8683) Since we have an inverse defined for matrices via `nonsing_inv`, we provide a `div_inv_monoid` instance for matrices. The instance provides the ability to refer to integer power of matrices via the auto-generated `gpow`. This is done in a new file to allow selective use. Many API lemmas are provided to facilitate usage of the new `gpow`, many copied in form/content from `algebra/group_with_zero/power.lean`, which provides a similar API.