prodMap_smul — Mathlib

English

Another variation of multiplicativity: f2' prodMap g2' times f1' prodMap g1' equals (f2' f1') prodMap (g2' g1').

Русский

Ещё одно свойство умножения: (f2' prodMap g2') (f1' prodMap g1') = (f2' f1') prodMap (g2' g1').

LaTeX

$$$ f'_2 \\text{ prodMap } g'_2 \\; * \\; f'_1 \\text{ prodMap } g'_1 = (f'_2 \\cdot f'_1) \\text{ prodMap } (g'_2 \\cdot g'_1). $$$

Lean4

@[simp]
theorem prodMap_smul [DistribMulAction S M₃] [DistribMulAction S M₄] [SMulCommClass R S M₃] [SMulCommClass R S M₄]
    (s : S) (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : prodMap (s • f) (s • g) = s • prodMap f g :=
  rfl

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