compAlternatingMap_smul — Mathlib

English

If S acts on N, then g.compAlternatingMap(s•f) = s•(g.compAlternatingMap f).

Русский

Если S действует на N, то композиция g с (s•f) равна s умножению на композицию g с f.

LaTeX

$$$ g.compAlternatingMap (s \cdot f) = s \cdot (g.compAlternatingMap f) $$$

Lean4

@[simp]
theorem compAlternatingMap_smul [Monoid S] [DistribMulAction S N] [DistribMulAction S N₂] [SMulCommClass R S N]
    [SMulCommClass R S N₂] [CompatibleSMul N N₂ S R] (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N) :
    g.compAlternatingMap (s • f) = s • g.compAlternatingMap f :=
  AlternatingMap.ext fun _ => g.map_smul_of_tower _ _

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