English
Let R be a ring with a star operation. If every pair of elements of a subset s commute, and every element of s commutes with the star of every element of s, then every pair of elements from s ∪ s* commute.
Русский
Пусть R — кольцо с операцией взятия звезды. Если любые две элементы подмножества s коммутируют между собой, и каждый элемент s коммутирует с сопряжённым элементом любого элемента из s, то любые два элемента из s ∪ s* коммутируют между собой.
LaTeX
$$$\\Big( \\forall x \\in s, \\forall y \\in s,\\ yx = xy \\Big) \\land \\Big( \\forall x \\in s, \\forall y \\in s,\\ y x^{\\ast} = x^{\\ast} y \\Big) \\Rightarrow \\ \\forall x \\in s \\cup s^{\\ast}, \\forall y \\in s \\cup s^{\\ast},\\ yx = xy$$$
Lean4
theorem union_star_self_comm (hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y)
(hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y) : ∀ x ∈ s ∪ star s, ∀ y ∈ s ∪ star s, y * x = x * y :=
by
change s ∪ star s ⊆ (s ∪ star s).centralizer
simp_rw [centralizer_union, ← star_centralizer, union_subset_iff, subset_inter_iff, star_subset_star, star_subset]
exact ⟨⟨hcomm, hcomm_star⟩, ⟨hcomm_star, hcomm⟩⟩
