English
If S and T are monoids acting on N with commuting scalar actions, then their actions commute on the space of alternating maps: for all s ∈ S, t ∈ T and f, (s • (t • f)) = (t • (s • f)).
Русский
Если S и T — моноиды, действующие на N с взаимно согласованными скалярами, то их действия на пространстве чередующихся отображений взаимно приводят к одному результату: ∀ s ∈ S, t ∈ T, f, s • (t • f) = t • (s • f).
LaTeX
$$$\forall s \in S, \forall t \in T, \forall f \in \operatorname{AlternatingMap}(R,M,N,\iota),\ s \cdot (t \cdot f) = t \cdot (s \cdot f).$$$
Lean4
instance instSMulCommClass {T : Type*} [Monoid T] [DistribMulAction T N] [SMulCommClass R T N] [SMulCommClass S T N] :
SMulCommClass S T (M [⋀^ι]→ₗ[R] N) where smul_comm _ _ _ := ext fun _ ↦ smul_comm ..
