Matrix Eigenvalues

Stream: mathlib4

[Bashar Hamade]

I am working on some proofs that require Linear Algebra properties , specifically properties on Eigenvalues of a Matrix of dimensions 'n x n' or its Spectral Radius , but I cannot seem to get access to some easy and intuitive way to work on that with the current implementations in Mathlib .

[Bashar Hamade]

to prove something like :

$$|eig(A)| < 1 \implies .... \forall A \in \mathbb{R}^{n \times n}$$

what would I need to import and how to approach it without overcomplicating the whole procedure

[Bashar Hamade]

my current implementation of matrix 'A' is something like :

A : Matrix (Fin n) (Fin n) ℝ

[Eric Wieser]

It's possible that https://github.com/eric-wieser/lean-matrix-cookbook will be useful to you, which you can use as a reference card between (some) matrix $\LaTeX$ and the corresponding Lean spellings