singleton_add_eq — Mathlib

English

For a ∈ A and r ∈ R, the spectrum of a shifted by r equals the spectrum of a plus r: {r} + σ(a) = σ(↑ₐ r + a).

Русский

Для a ∈ A и r ∈ R спектр элемента a со смещением на r равен спектру элемента a + φ(r): {r} + σ(a) = σ(φ(r) + a).

LaTeX

$$$\{r\} + \sigma(a) = \sigma(\uparrow\!a\; r + a)$$$

Lean4

theorem singleton_add_eq (a : A) (r : R) : { r } + σ a = σ (↑ₐ r + a) :=
  ext fun x => by rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]

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