English
For any nonzero nonunit r, r belongs to the quasispectrum of a for any a in a module over R.
Русский
Для любого неединичного неединичного r, элемент r принадлежит квазиспектру a для любого a в модуле над R.
LaTeX
$$$$ \forall a, \forall r \; (\neg IsUnit(r)) \Rightarrow r \in \operatorname{quasispectrum}(R,a) $$$$
Lean4
/-- If `A` is a non-unital `R`-algebra, the `R`-quasispectrum of `a : A` consists of those `r : R`
such that if `r` is invertible (in `R`), then `-(r⁻¹ • a)` is not quasiregular.
The quasispectrum is precisely the spectrum in the unitization when `R` is a commutative ring.
See `Unitization.quasispectrum_eq_spectrum_inr`. -/
def quasispectrum (a : A) : Set R :=
{r : R | (hr : IsUnit r) → ¬IsQuasiregular (-(hr.unit⁻¹ • a))}
