mem_iff_of_isUnit — Mathlib

English

For a commutative semiring R and nonunital ring A with module structure, if r is a unit, membership in quasispectrum is equivalent to a non-quasiregular condition.

Русский

Для единицы r и соответствующих структур: принадлежность к квазиспектруму равна некорректному условию из IsQuasiregular.

LaTeX

$$$r \in quasispectrum_R(a) \iff \neg IsQuasiregular(- (hr.unit^{-1} \cdot a))$$$

Lean4

theorem mem_iff_of_isUnit [CommSemiring R] [NonUnitalRing A] [Module R A] {a : A} {r : R} (hr : IsUnit r) :
    r ∈ quasispectrum R a ↔ ¬IsQuasiregular (-(hr.unit⁻¹ • a)) :=
  ⟨fun h => h hr, fun h _ => h⟩

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