notMem_iff

Mathlib.Algebra.Algebra.Spectrum.Basic

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

English

For r ∈ R and a ∈ A, r ∈ spectrum(a) iff not IsUnit (algebraMap r − a).

Русский

Для r ∈ R и a ∈ A верно: r ∈ спектр(a) тогда и только тогда, когда не является единицей (algebraMap r − a).

LaTeX

$$$r \in \sigma(a) \;\Leftrightarrow\; \neg \operatorname{IsUnit}(\uparrow r - a)$$$

Lean4

theorem notMem_iff {r : R} {a : A} : r ∉ σ a ↔ IsUnit (↑ₐ r - a) := by simp [mem_iff]

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

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

Разделы

Аффилиация

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