mem_commutant_iff — Mathlib

English

An element z lies in the commutant of S if and only if z commutes with every element of S.

Русский

Элемент z лежит в коммутанте S тогда и только тогда, когда z коммутирует с каждым элементом S.

LaTeX

$$$z \\in S.commutant \\iff \\forall g \\in S, g z = z g$$$

Lean4

@[simp]
theorem mem_commutant_iff {S : VonNeumannAlgebra H} {z : H →L[ℂ] H} : z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g :=
  by
  rw [← SetLike.mem_coe, coe_commutant]
  rfl

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