resolventSet — Mathlib

English

For a ∈ A, the resolvent set consists of those r ∈ R for which r•1 − a is invertible in A.

Русский

Для a ∈ A множество разрешённых значений состоит из тех r ∈ R, для которых r·1 − a является обратимым в A.

LaTeX

$$$\operatorname{resolventSet}(a) = \{ r \in R \mid \operatorname{IsUnit}(\uparrow a r - a) \}$$$

Lean4

/-- Given a commutative ring `R` and an `R`-algebra `A`, the *resolvent set* of `a : A`
is the `Set R` consisting of those `r : R` for which `r•1 - a` is a unit of the
algebra `A`. -/
def resolventSet (a : A) : Set R :=
  {r : R | IsUnit (↑ₐ r - a)}

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