instSMulCommClassSubtypeMemSubmonoidCenter

English

There is an SMulCommClass instance for the action of R on the center of Submonoid, compatible with the subtype action.

Русский

Существует экземпляр SMulCommClass для действия R на центр Submonoid, совместимый с действием подтипа.

LaTeX

$$$ \text{instance } : SMulCommClass \\ R \\ (Submonoid.center R) M $$$

Lean4

instance : SMulCommClass R (Submonoid.center R) M where
  smul_comm r r' m := by simp_rw [Submonoid.smul_def, smul_smul, ((Set.mem_center_iff.1 r'.prop).1 _).eq]

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