zero_notMem_iff

Mathlib.Algebra.Algebra.Spectrum.Basic

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

English

For a unit a ∈ A, 0 is not in the spectrum of a.

Русский

Для единицы a ∈ A 0 не принадлежит спектру a.

LaTeX

$$$0 \notin \sigma(a) \quad\text{for } a \in A^{\times}$$$

Lean4

theorem zero_notMem_iff {a : A} : (0 : R) ∉ σ a ↔ IsUnit a := by rw [zero_mem_iff, Classical.not_not]

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

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

Разделы

Аффилиация

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