instFactMemSetQuasispectrumOfNat — Mathlib

English

For a commutative base ring R and a nonunital algebra A with a predicate p, zero belongs to the quasispectrum of a whenever a satisfies p.

Русский

При заданном p ноль принадлежит квазиспектру а при условии, что a удовлетворяет p.

LaTeX

$$0 \in σ_n R a$$

Lean4

instance {R A : Type*} [CommSemiring R] [NonUnitalRing A] [Module R A] [Nontrivial R] (a : A) : Fact (0 ∈ σₙ R a) :=
  ⟨quasispectrum.zero_mem R a⟩

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