instIsCentralScalar — Mathlib

English

The space of continuous alternating maps inherits a central scalar structure from the base scalars, meaning scalars act centrally on AltMaps.

Русский

Пространство непрерывных чередующих отображений наследует центральную структуру скаляров от базовых, то есть скаляры действуют централизованно на AltMap.

LaTeX

$$$ IsCentralScalar R' (ContinuousAlternatingMap A M N ι) $$$

Lean4

instance [DistribMulAction R'ᵐᵒᵖ N] [IsCentralScalar R' N] : IsCentralScalar R' (M [⋀^ι]→L[A] N) :=
  ⟨fun _ _ => ext fun _ => op_smul_eq_smul _ _⟩

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