spectralRadius_zero

Mathlib.Analysis.Normed.Algebra.Spectrum

URI: https://scilib.ai/kg/mathlib#spectrum.spectralRadius_zero

English

The spectral radius of 0 is 0.

Русский

Спектральный радиус нуля равен нулю.

LaTeX

$$$\operatorname{spectralRadius}(\mathbb{K}, 0) = 0.$$$

Lean4

@[simp]
theorem spectralRadius_zero : spectralRadius 𝕜 (0 : A) = 0 :=
  by
  nontriviality A
  simp [spectralRadius]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru