Commit 2025-08-08 14:49 a5b4f3bc

View on Github →

feat: add lemmas on spectralRadius along with supporting lemmas (#27993) Added new lemmas on spectralRadius and spectrum, and removed unnecessary assumptions from some existing spectralRadius lemmas. Also introduced lemmas involving iSup₂ and iInf₂.

Estimated changes

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

modified theorem spectrum.SpectralRadius.of_subsingleton

modified theorem spectrum.mem_resolventSet_of_spectralRadius_lt

added theorem spectrum.spectralRadius_one

added theorem spectrum.spectralRadius_pow_le'

added theorem spectrum.spectralRadius_pow_le

Modified Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean

added theorem spectrum.pow_mem_pow

Modified Mathlib/Order/CompleteLattice/Basic.lean

added theorem OrderIso.map_iInf₂

added theorem OrderIso.map_iSup₂

Modified Mathlib/Topology/Instances/NNReal/Lemmas.lean

added theorem ENNReal.iSup₂_pow_of_ne_zero