instIsCentralScalar — Mathlib

English

Given the scalar action data, CentroidHom α inherits a central scalar structure from M.

Русский

С учетом данных действия скаляров CentroidHom α наследует структуру центрального скаляра от M.

LaTeX

$$IsCentralScalar M (CentroidHom α)$$

Lean4

instance [DistribMulAction Mᵐᵒᵖ α] [IsCentralScalar M α] : IsCentralScalar M (CentroidHom α) where
  op_smul_eq_smul _ _ := ext fun _ => op_smul_eq_smul _ _

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