eq — Mathlib · SciLib

English

If h is a semiconjugacy between a, x, y, then a x = y a.

Русский

Если h задаёт полусопряжение между a, x, y, то выполняется a x = y a.

LaTeX

$$$$h:\ SemiconjBy\ a\ x\ y\Rightarrow a x = y a.$$$$

Lean4

/-- Equality behind `SemiconjBy a x y`; useful for rewriting. -/
@[to_additive /-- Equality behind `AddSemiconjBy a x y`; useful for rewriting. -/
    ]
protected theorem eq [Mul S] {a x y : S} (h : SemiconjBy a x y) : a * x = y * a :=
  h

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