centralizer_centralizer_comm_of_comm

English

If S commutes pairwise within itself, then any two elements of S.centralizer.centralizer commute with each other.

Русский

Если элементы S парно коммутируют между собой, то любые два элемента из S.centralizer.centralizer коммутируют между собой.

LaTeX

$$$ (\forall x \in S, \forall y \in S, xy = yx) \Rightarrow \forall x \in S.centralizer.centralizer, \forall y \in S.centralizer.centralizer, xy = yx $$$

Lean4

@[to_additive addCentralizer_addCentralizer_comm_of_comm]
theorem centralizer_centralizer_comm_of_comm (h_comm : ∀ x ∈ S, ∀ y ∈ S, x * y = y * x) :
    ∀ x ∈ S.centralizer.centralizer, ∀ y ∈ S.centralizer.centralizer, x * y = y * x := fun _ h₁ _ h₂ ↦
  h₂ _ fun _ h₃ ↦ h₁ _ fun _ h₄ ↦ h_comm _ h₄ _ h₃

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