English
Let α be a monoid. For elements a, x, y ∈ α, the semiconjugacy relation is preserved under taking opposites: SemiconjBy (op a) (op y) (op x) holds if and only if SemiconjBy a x y holds.
Русский
Пусть α — моноид. Пусть элементы a, x, y принадлежат α. Полу сопряжённость сохраняется под противоположностью: SemiconjBy (op a) (op y) (op x) выполняется тогда и только тогда, когда SemiconjBy a x y выполняется.
LaTeX
$$$\\SemiconjBy\\ (\\operatorname{op} a)\\ (\\operatorname{op} y)\\ (\\operatorname{op} x)\\ \\iff\\ \\SemiconjBy\\ a\\ x\\ y$$$
Lean4
@[to_additive (attr := simp)]
theorem semiconjBy_op [Mul α] {a x y : α} : SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y := by
simp only [SemiconjBy, ← op_mul, op_inj, eq_comm]
