instIsCentralScalar — Mathlib

English

The scalar action of S is central on the space of alternating maps; i.e., for every c ∈ S and f in AlternatingMap, c • f = f • c.

Русский

Действие скаляра S на пространство чередующихся отображений центрально: для каждого c ∈ S и f ∈ AlternatingMap выполняется c • f = f • c.

LaTeX

$$$\forall s \in S, \forall f \in \operatorname{AlternatingMap}(R,M,N,\iota),\ s \cdot f = f \cdot s.$$$

Lean4

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

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