instIsCentralScalar — Mathlib

English

ZeroHom has a central scalar action: IsCentralScalar M (ZeroHom A B) given SMulZeroClass on M and B and IsCentralScalar.

Русский

ZeroHom имеет центральное скалярное действие: IsCentralScalar M (ZeroHom A B) при наличии SMulZeroClass и IsCentralScalar.

LaTeX

$$[SMulZeroClass M B] [SMulZeroClass Mᵐᵒᵖ B] [IsCentralScalar M B] : IsCentralScalar M (ZeroHom A B)$$

Lean4

instance [SMulZeroClass M B] [SMulZeroClass Mᵐᵒᵖ B] [IsCentralScalar M B] : IsCentralScalar M (ZeroHom A B) where
  op_smul_eq_smul _ _ := ext fun _ => op_smul_eq_smul _ _

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