spectrum — Mathlib

English

The spectrum of a is the complement of its resolvent set: σ(a) = R \ resolventSet(a).

Русский

Спектр a есть дополнение к множеству разрешённых значений: σ(a) = R \ ResolventSet(a).

LaTeX

$$$\sigma(a) = R \setminus \operatorname{resolventSet}(a)$$$

Lean4

/-- Given a commutative ring `R` and an `R`-algebra `A`, the *spectrum* of `a : A`
is the `Set R` consisting of those `r : R` for which `r•1 - a` is not a unit of the
algebra `A`.

The spectrum is simply the complement of the resolvent set. -/
def spectrum (a : A) : Set R :=
  (resolventSet R a)ᶜ

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