adjoin_le_centralizer_centralizer

English

The subalgebra generated by a set s lies inside the centralizer of the centralizer of s; i.e., every element built from s commutes with every element that commutes with all elements of s.

Русский

Подалгебра, порождаемая множеством s, содержится в централизаторе централизатора s; то есть каждый элемент, полученный из s, commuting с каждым элементом, который commute с каждым элементом s.

LaTeX

$$$\operatorname{adjoin}_R(s) \subseteq \operatorname{centralizer}_R(\operatorname{centralizer}_R(s)).$$$

Lean4

theorem adjoin_le_centralizer_centralizer (s : Set A) : adjoin R s ≤ centralizer R (centralizer R s) :=
  by
  rw [← toSubalgebra_le_iff, centralizer_toSubalgebra, adjoin_toSubalgebra]
  convert Algebra.adjoin_le_centralizer_centralizer R (s ∪ star s)
  rw [StarMemClass.star_coe_eq]
  simp

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