comp_smul — Mathlib

English

A specialization of comp_smul with identity ring hom id, showing compatibility of scalar action with composition.

Русский

Специализация comp_smul для тождественного кольра: совместимость скалярного действия и композиции.

LaTeX

$$comp_smul (RingHom.id R) a f = a • (f)$$

Lean4

theorem comp_smul [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [DistribMulAction S M₃] [SMulCommClass R S M₃]
    [CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) : g.comp (a • f) = a • g.comp f :=
  ext fun _ ↦ g.map_smul_of_tower _ _

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