English
If a lies in the center of a ring, then its star is also in the center.
Русский
Если элемент лежит в центре кольца, то его звезда также лежит в центре.
LaTeX
$$$a \\in \\mathrm{center}(R) \\Rightarrow \\ star\\ a \\in \\mathrm{center}(R).$$$
Lean4
theorem star_mem_center (ha : a ∈ Set.center R) : star a ∈ Set.center R
where
comm := by simpa only [star_mul, star_star] using fun g => congr_arg star ((mem_center_iff.1 ha).comm <| star g).symm
left_assoc b
c :=
calc
star a * (b * c) = star a * (star (star b) * star (star c)) := by rw [star_star, star_star]
_ = star a * star (star c * star b) := by rw [star_mul]
_ = star ((star c * star b) * a) := by rw [← star_mul]
_ = star (star c * (star b * a)) := by rw [ha.right_assoc]
_ = star (star b * a) * c := by rw [star_mul, star_star]
_ = (star a * b) * c := by rw [star_mul, star_star]
right_assoc b
c :=
calc
b * c * star a = star (a * star (b * c)) := by rw [star_mul, star_star]
_ = star (a * (star c * star b)) := by rw [star_mul b]
_ = star ((a * star c) * star b) := by rw [ha.left_assoc]
_ = b * star (a * star c) := by rw [star_mul, star_star]
_ = b * (c * star a) := by rw [star_mul, star_star]
