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:
- ```
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