zero_eq — Mathlib

English

For units a: r ∈ spectrum R a ↔ r⁻¹ ∈ spectrum R a⁻¹.

Русский

Для единицы a: r ∈ σ(a) ↔ r⁻¹ ∈ σ(a⁻¹).

LaTeX

$$$ r \in \sigma_R(a) \iff r^{-1} \in \sigma_R(a^{-1}) $$$

Lean4

/-- Without the assumption `Nontrivial A`, then `0 : A` would be invertible. -/
@[simp]
theorem zero_eq [Nontrivial A] : σ (0 : A) = {0} :=
  by
  refine Set.Subset.antisymm ?_ (by simp [Algebra.algebraMap_eq_smul_one, mem_iff])
  rw [spectrum, Set.compl_subset_comm]
  intro k hk
  rw [Set.mem_compl_singleton_iff] at hk
  have : IsUnit (Units.mk0 k hk • (1 : A)) := IsUnit.smul (Units.mk0 k hk) isUnit_one
  simpa [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one]

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