spectrum_algebraMap_subset — Mathlib

English

Re-states the spectrum equality for algebraMap: spectrum R (algebraMap R A r) = {r}.

Русский

Повторное утверждение спектра для algebraMap: спектр равен {r}.

LaTeX

$$spectrum R (algebraMap R A r) = { r }$$

Lean4

theorem spectrum_algebraMap_subset (r : R) : spectrum R (algebraMap R A r) ⊆ { r } :=
  by
  rw [← cfc_const r 0 (cfc_predicate_zero R), cfc_map_spectrum (fun _ ↦ r) 0 (cfc_predicate_zero R)]
  rintro - ⟨x, -, rfl⟩
  simp

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