No matrix powers

Stream: new members

[Damien Thomine]

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]

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]

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

[Damien Thomine]

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]

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

[Alex J. Best]

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