subset_singleton_zero_compl

Mathlib.Algebra.Algebra.Spectrum.Basic

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

← MathLib Explorer

English

If a is a unit, spectrum(a) is contained in the complement of {0}.

Русский

Если a является единицей, спектр(a) ⊆ {0}^c.

LaTeX

$$$\sigma(a) \subseteq \{0\}^{c} \quad\text{when } a \in A^{\times}$$$

Lean4

theorem subset_singleton_zero_compl {a : A} (ha : IsUnit a) : spectrum R a ⊆ {0}ᶜ :=
  Set.subset_compl_singleton_iff.mpr <| spectrum.zero_notMem R ha

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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