star_mem_resolventSet_iff — Mathlib

English

For r ∈ R and a ∈ A, star r ∈ resolventSet R a iff r ∈ resolventSet R (star a).

Русский

Для r ∈ R и a ∈ A: star r ∈ резольвентное множество a тогда и только тогда, когда r ∈ резольвентное множество star a.

LaTeX

$$$\star r \in \operatorname{resolventSet}(R,a) \iff r \in \operatorname{resolventSet}(R, \star a)$$$

Lean4

theorem star_mem_resolventSet_iff {r : R} {a : A} : star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a) := by
  refine ⟨fun h => ?_, fun h => ?_⟩ <;>
    simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul, star_star, star_one] using
      IsUnit.star h

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