Calculating trace of a non-square SciLean matrix

Stream: new members

[frisbro]

Hi all,
I ran into this problem trying to implement a custom trace function of general matrices:

import SciLean

open Scilean
open Finset

def trace {n m : Nat} (A : Float^[n,m]): Float :=
  ∑ k in range (min n m), A[⟨k, sorry⟩, ⟨k, sorry⟩]

It seems that I would need to prove that k is in Fin n and k is in Fin m, but I'm not sure how to proceed. Sorry for what is probably a very basic question?

Best regards, Felix

[Aaron Liu]

This is not a #mwe, so I can't know exactly what problem you're having, but try summing ∑ k : Fin (min n m), A[k.castLE (min_le_left n m), k.castLE (min_le_right n m)] instead?

[frisbro]

I apologize for not posting a mwe, I've updated the question to include the opens and import. Thank you for your answer, that indeed solved the problem!