zero_mem — Mathlib

English

There is a zero element in the quasispectrum set, defined as the pair consisting of zero and the proof of membership?

Русский

В множестве quasispectrum существует нулевой элемент, заданный как пара и доказательство принадлежности.

LaTeX

$$$$ \text{Zero in }\operatorname{quasispectrum}(R,a) $$$$

Lean4

@[simp]
theorem zero_mem [Nontrivial R] (a : A) : 0 ∈ quasispectrum R a :=
  quasispectrum.not_isUnit_mem a <| by simp

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