mem_resolventSet_apply — Mathlib

English

Let φ: A → B be an algebra homomorphism. Then σ(φ(a)) ⊆ σ(a) for all a ∈ A.

Русский

Пусть φ: A → B — алгебраическое гомоморфизм. Тогда σ(φ(a)) ⊆ σ(a) для всех a ∈ A.

LaTeX

$$$\sigma_R((\phi : A \to B) a) \subseteq \sigma_R(a)$$$

Lean4

theorem mem_resolventSet_apply (φ : F) {a : A} {r : R} (h : r ∈ resolventSet R a) :
    r ∈ resolventSet R ((φ : A → B) a) := by simpa only [map_sub, AlgHomClass.commutes] using h.map φ

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