Jordan Canonical Form

Stream: new members

[eren uyanık]

Hi all, I am new to LEAN and trying to implement some basic definitions of Jordan Canonical Form. Few questions:

1. ```
   def jordanBlock (eig : ℕ) (n : ℕ) : Matrix (Fin n) (Fin n) ℕ :=
   Matrix.of fun i j =>
   if i = j then eig
   else if i = j.succ then 1
   else 0

1.1 Why do I need to use '.succ' instead of '+ 1'?
1.2 I could not make the matrix inputs from \C.
In both cases, I get the error (first one with 'Fin' type instead of '\C')
"failed to synthesize
  OfNat ℂ 0
numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
  ℂ
due to the absence of the instance above"

[Ilmārs Cīrulis]

import Mathlib

def jordanBlock (eig : ℂ) (n : ℕ) : Matrix (Fin n) (Fin n) ℂ :=
  Matrix.of
  (fun (i j: Fin n) =>
   if i.val = j.val then eig
   else if i.val = j.val + 1 then 1
   else 0)

Maybe this work for you?

[Robin Arnez]

1.1 if you do + 1 then it needs to verify for 1 that there is an element of Fin n, i.e. that n is nonzero. You might say "but it's right there, i and j are values of Fin n!", well lean is not smart enough to figure that out on its own and you need to tell it that n is nonzero:
haveI : NeZero n := NeZero.of_pos (Fin.pos i)
In your case, j.succ is the value above j within Fin (n + 1) (not Fin n!) so it added weird coercions to make Fin n into Fin (n + 1). That's a bit fragile though so it's better to decide on which one you want to use:
(a) i.val = j.val + 1: In the example of Fin 4, matches 1, 0, 2, 1, 3, 2 (not 0, 3!)
(b) i = j + 1: In the example of Fin 4, matches 1, 0, 2, 1, 3, 2 and 0, 3
1.2 sounds like you're missing the import (import Mathlib.Data.Complex.Basic) and it made an auto-implicit.

So fixed it is:

import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Defs

def jordanBlock (eig : ℂ) (n : ℕ) : Matrix (Fin n) (Fin n) ℂ :=
  Matrix.of fun i j =>
    haveI : NeZero n := NeZero.of_pos (Fin.pos i)
    if i = j then eig
    else if i = j + 1 then 1
    else 0

If the 1 still doesn't work then you might need to upgrade to a later version of lean.