isCentralScalar — Mathlib

English

If M acts centrally on α and β, then M acts centrally on α×β.

Русский

Если M действует центрированно на α и на β, то и на α×β действует центрированно.

LaTeX

$$$IsCentralScalar\\ M (α) \\wedge IsCentralScalar\\ M (β) \\Rightarrow IsCentralScalar\\ M (α × β)$$$

Lean4

@[to_additive]
instance isCentralScalar [SMul Mᵐᵒᵖ α] [SMul Mᵐᵒᵖ β] [IsCentralScalar M α] [IsCentralScalar M β] :
    IsCentralScalar M (α × β) where op_smul_eq_smul _ _ := Prod.ext (op_smul_eq_smul _ _) (op_smul_eq_smul _ _)

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