Zulip Chat Archive

Stream: new members

Topic: d to


view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:08):

I was suprised it worked. I wrote:

def Gaussian_elimination6 {α : Type v} [ordered_ring α]  :
   Π (m n), matrix (fin m) (fin n) α   α
| (x+1) (y+1) A := A 0 0
| _ _ A := A 0 0

Last updated: May 11 2021 at 22:14 UTC