## Stream: new members

### Topic: No matrix powers

#### Damien Thomine (Feb 06 2022 at 19:26):

I've tried to play with matrices, but apparently Lean does not know what a power of a matrix is.

import tactic
import data.matrix.basic

variables (n : Type*) [fintype n] (A : matrix n n ℤ) (m : ℕ)

example : monoid (matrix n n ℤ) := by apply_instance,

#check A^m


Apparently, there is no instance of monoid (or ring, or probably many other things) for finite square matrices. How do I plug this gap?

#### Alex J. Best (Feb 06 2022 at 19:36):

There is docs#matrix.ring so possibly all you need is to asssume [decidable_eq n] or run open_locale classical (both untested)

#### Eric Wieser (Feb 06 2022 at 22:04):

Right, you need to be able to decide equality of n to populate the diagonal of the identity matrix

#### Damien Thomine (Feb 08 2022 at 01:02):

Thank you both, that fixed both problems (apply_instance does not work, but an explicit appeal to matrix.ring does, and the check also works).

#### Alex J. Best (Feb 08 2022 at 01:04):

There shouldn't be a comma after apply_instance is the only issue I see

#### Alex J. Best (Feb 08 2022 at 01:05):

This works without warnings/errors

import tactic
import data.matrix.basic

variables (n : Type*) [fintype n] [decidable_eq n] (A : matrix n n ℤ) (m : ℕ)

example : monoid (matrix n n ℤ) := by apply_instance

#check A^m


Last updated: Dec 20 2023 at 11:08 UTC