Gelfand's spectral radius formula

Stream: Is there code for X?

[Bashar Hamade]

Hello , is there some sort of implementation already available for Gelfand's spectral radius formula :

$$\rho(A) = \lim_{n \to \infty} \|A^n\|^{1/n}$$

[Kenny Lau]

@Bashar Hamade Leansearch, "Gelfand's spectral radius formula"

[Kenny Lau]

image.png

leanprover-community.github.io/mathlib4_docs/find/?pattern=spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius#doc

[Bashar Hamade]

Kenny Lau said:

Bashar Hamade Leansearch, "Gelfand's spectral radius formula"

nice,thank you !