op — Mathlib · SciLib

English

If h is a semiconjugacy between a, x, y in a monoid, then taking opposites yields a semiconjugacy: SemiconjBy (op a) (op y) (op x).

Русский

Если существует полу сопряжение между a, x, y, то взятие противоположностей даёт полу сопряжение: SemiconjBy (op a) (op y) (op x).

LaTeX

$$$\\text{If } h: \\SemiconjBy a x y, \\text{ then } \\SemiconjBy (\\operatorname{op} a) (\\operatorname{op} y) (\\operatorname{op} x).$$$

Lean4

@[to_additive]
theorem _root_.SemiconjBy.op [Mul α] {a x y : α} (h : SemiconjBy a x y) : SemiconjBy (op a) (op y) (op x) :=
  semiconjBy_op.2 h

Похожие утверждения