opposite_smulCommClass — Mathlib

English

For a semigroup α, the left action of αᵐᵒᵖ on α commutes with the right action of α on α, i.e., αᵐᵒᵖ and α commute on α.

Русский

Для полугруппы α лево-действие αᵐᵒᵖ на α совместимо с правым действием α на α; т.е. αᵐᵒᵖ и α коммутируют на α.

LaTeX

$$$\text{SMulCommClass } α^{\mathrm{op}} \; α \; α$$$

Lean4

@[to_additive]
instance opposite_smulCommClass [Semigroup α] : SMulCommClass αᵐᵒᵖ α α where smul_comm _ _ _ := mul_assoc _ _ _

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