English
Conjugation by a unit preserves the spectrum: spectrum_R(u a u⁻¹) = spectrum_R(a).
Русский
Суперпозиция по единице сохраняет спектр: spectrum_R(u a u⁻¹) = spectrum_R(a).
LaTeX
$$$\operatorname{spectrum}_R(u a u^{-1}) = \operatorname{spectrum}_R(a)$$$
Lean4
@[simp]
theorem spectrum_eq {F R A B : Type*} [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] [EquivLike F A B]
[AlgEquivClass F R A B] (f : F) (a : A) : spectrum R (f a) = spectrum R a :=
Set.Subset.antisymm (AlgHom.spectrum_apply_subset _ _) <| by
simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using
AlgHom.spectrum_apply_subset (f : A ≃ₐ[R] B).symm (f a)