zero_mem_iff

Mathlib.Algebra.Algebra.Spectrum.Basic

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

English

0 ∈ spectrum(a) iff a is not a unit.

Русский

0 принадлежит спектру(a) тогда и только тогда, когда a не является единицей.

LaTeX

$$$0 \in \sigma(a) \iff \neg \operatorname{IsUnit}(a)$$$

Lean4

theorem zero_mem_iff {a : A} : (0 : R) ∈ σ a ↔ ¬IsUnit a := by rw [mem_iff, map_zero, zero_sub, IsUnit.neg_iff]

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

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

Разделы

Аффилиация

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