mathlib3

99c634cc - feat(analysis/normed_space/spectrum): adds easy direction of Gelfand's formula for the spectral radius (#10847)

feat(analysis/normed_space/spectrum): adds easy direction of Gelfand's formula for the spectral radius (#10847) This adds the easy direction (i.e., an inequality) of Gelfand's formula for the spectral radius. Namely, we prove that `spectral_radius 𝕜 a ≤ ∥a ^ (n + 1)∥₊ ^ (1 / (n + 1) : ℝ)` for all `n : ℕ` using the spectral mapping theorem for polynomials. - [x] depends on: #10783