isCentralScalar — Mathlib

English

If α is a commutative semigroup, then α is a central scalar object for itself: op_smul_eq_smul holds, i.e., m • a = a • m for all m,a ∈ α.

Русский

Если α — коммутативная полугруппа, то она является центральным скаляром для самого себя: op_smul_eq_smul, то есть m • a = a • m.

LaTeX

$$$[CommSemigroup\ α]\;:\; IsCentralScalar α α\,\text{ with } op\_smul\_eq\_smul\ _:= mul\_comm _ _$$$

Lean4

@[to_additive]
instance isCentralScalar [CommSemigroup α] : IsCentralScalar α α where op_smul_eq_smul _ _ := mul_comm _ _

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