English
Let R be a star-ring (a ring with an involutive anti-automorphism). If x and y are self-adjoint, then x and y commute if and only if their product xy is self-adjoint.
Русский
Пусть R — кольцо со звездо-инволюцией. Если x и y самосопряжённы, то они коммутируют тогда и только тогда, когда произведение xy самосопряжено.
LaTeX
$$$\text{Commute}(x,y) \iff \text{IsSelfAdjoint}(xy)$$$
Lean4
/-- Self-adjoint elements commute if and only if their product is self-adjoint. -/
theorem commute_iff {R : Type*} [Mul R] [StarMul R] {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) :
Commute x y ↔ IsSelfAdjoint (x * y) := by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rw [isSelfAdjoint_iff, star_mul, hx.star_eq, hy.star_eq, h.eq]
· simpa only [star_mul, hx.star_eq, hy.star_eq] using h.symm
