English
The relation SemiconjBy is preserved under star: SemiconjBy(star x)(star z)(star y) iff SemiconjBy x y z.
Русский
Отношение полуправосопряженности сохраняется под звездой: SemiconjBy(star x)(star z)(star y) эквивалентно SemiconjBy x y z.
LaTeX
$$$$ \operatorname{SemiconjBy}(\star x)(\star z)(\star y) \iff \operatorname{SemiconjBy}(x)(y)(z). $$$$
Lean4
@[simp]
theorem semiconjBy_star_star_star {x y z : R} : SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z := by
simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]