mem_of_not_quasiregular — Mathlib

English

Let a ∈ A and r ∈ R^×. If -(r⁻¹ · a) is not quasiregular, then r belongs to the quasispectrum of a.

Русский

Пусть a ∈ A и r ∈ R^×. Если -(r⁻¹ · a) не квазирегулярно, то r принадлежит к квазиспектруму a.

LaTeX

$$$- (r^{-1} \\cdot a)$ не quasiregular ⇒ (r : R) \\in \\mathrm{quasispectrum}(R,a)$$$

Lean4

theorem mem_of_not_quasiregular (a : A) {r : Rˣ} (hr : ¬IsQuasiregular (-(r⁻¹ • a))) : (r : R) ∈ quasispectrum R a :=
  fun _ ↦ by simpa using hr

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