smul_compAlternatingMap — Mathlib

English

Another variant of smul compatibility for AltMap with left action.

Русский

Ещё одна форма совместимости умножения AltMap со слева.

LaTeX

$$$ g \circ_{\mathrm{Alt}} (s \cdot f) = s \cdot (g \circ_{\mathrm{Alt}} f) $$$

Lean4

@[simp]
theorem smul_compAlternatingMap [Monoid S] [DistribMulAction S N₂] [SMulCommClass R S N₂] (g : N →ₗ[R] N₂) (s : S)
    (f : M [⋀^ι]→ₗ[R] N) : (s • g).compAlternatingMap f = s • g.compAlternatingMap f :=
  rfl

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