nonzero_mul_comm — Mathlib

English

The spectrum of a product ab, with zero removed, is independent of order: σ(ab) \ {0} = σ(ba) \ {0}.

Русский

Спектр произведения ab без нуля не зависит от порядка: σ(ab) \ {0} = σ(ba) \ {0}.

LaTeX

$$$\sigma_R(a b) \setminus \{0\} = \sigma_R(b a) \setminus \{0\}$$$

Lean4

theorem nonzero_mul_comm (a b : A) : σ (a * b) \ {0} = σ (b * a) \ {0} :=
  by
  suffices h : ∀ x y : A, σ (x * y) \ {0} ⊆ σ (y * x) \ {0} from Set.eq_of_subset_of_subset (h a b) (h b a)
  rintro _ _ k ⟨k_mem, k_neq⟩
  change ((Units.mk0 k k_neq) : 𝕜) ∈ _ at k_mem
  exact ⟨unit_mem_mul_comm.mp k_mem, k_neq⟩

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