spectrum_algebraMap_eq — Mathlib

English

Same as above, under the nontriviality assumption, spectrum of algebraMap R A r equals {r}.

Русский

То же самое при условии не тривиальности: спектр algebraMap R A r равен {r}.

LaTeX

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

Lean4

theorem spectrum_algebraMap_eq [Nontrivial A] (r : R) : spectrum R (algebraMap R A r) = { r } :=
  by
  have hp : p 0 := cfc_predicate_zero R
  rw [← cfc_const r 0 hp, cfc_map_spectrum (fun _ => r) 0 hp]
  exact Set.Nonempty.image_const (⟨0, spectrum.zero_mem (R := R) not_isUnit_zero⟩) _

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