instSMulCommClass — Mathlib

English

The action of S on End_R(M) commutes with composition: (s • f) ∘ g = f ∘ (s • g).

Русский

Действие S на End_R(M) коммутирует с композиционным умножением: (s • f) ∘ g = f ∘ (s • g).

LaTeX

$$$ (s \cdot f) \circ g = f \circ (s \cdot g) $$$

Lean4

instance instSMulCommClass [SMul S R] [IsScalarTower S R M] : SMulCommClass S (Module.End R M) (Module.End R M) :=
  ⟨fun s _ _ ↦ (comp_smul _ s _).symm⟩

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