Summing entries of matrix

Stream: new members

[Aron Erben]

Hello

I'm trying to sum the entries of a matrix (n x 1). I've been trying it with finset.sum, but it does not seem to work, here is an MWE:

import data.matrix.basic
import data.real.basic
import algebra.big_operators.basic

variables {n : ℕ} (m : matrix (fin n) unit ℝ)

#check ∑ i in finset.range n, m i 0

Which gives the error:

10:31: type mismatch at application
  m i
term
  i
has type
  ℕ
but is expected to have type
  fin n

I understand why the error happens. I'm wondering if there is an easy canonical way to do this using mathlib.

Thanks in advance!

[Johan Commelin]

Just leave out the in finset.range n.

[Johan Commelin]

That's forcing i to be a natural number, whereas you want something in fin n.