map_inv

Mathlib.Algebra.Algebra.Spectrum.Basic

URI: https://scilib.ai/kg/mathlib#spectrum.map_inv

English

For a unit a ∈ A, σ(a)⁻¹ = σ(a⁻¹).

Русский

Для единицы a: спектр инвертированного элемента равен спектру обратного элемента: σ(a)⁻¹ = σ(a⁻¹).

LaTeX

$$$(\sigma_R(a))^{-1} = \sigma_R(a^{-1})$$$

Lean4

protected theorem map_inv (a : Aˣ) : (σ (a : A))⁻¹ = σ (↑a⁻¹ : A) :=
  by
  ext
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru