instIsCentralScalar — Mathlib

English

There is an IsScalarTower structure for ContinuousMultilinearMap over a pair of rings, ensuring compatibility of scalar actions across layers.

Русский

Существует структура IsScalarTower для ContinuousMultilinearMap над парой колец, обеспечивающая совместимость действий скаляров по слоям.

LaTeX

$$$\\text{IsScalarTower }(R',R'',\\mathrm{ContinuousMultilinearMap} A M_1 M_2).$$$

Lean4

instance [DistribMulAction R'ᵐᵒᵖ M₂] [IsCentralScalar R' M₂] : IsCentralScalar R' (ContinuousMultilinearMap A M₁ M₂) :=
  ⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

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