Commit 2021-12-24 15:31 99c634cc

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.

• depends on: #10783