Zulip Chat Archive

Stream: new members

Topic: Jordan Canonical Form


eren uyanık (Apr 21 2025 at 21:06):

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 (Apr 21 2025 at 21:19):

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 (Apr 23 2025 at 19:49):

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.


Last updated: May 02 2025 at 03:31 UTC