instIsScalarTower — Mathlib

English

There is a scalar tower structure: S acts on End_R(M) in a way that is compatible with composition, i.e., smul_comp holds: (s • f) ∘ g = s • (f ∘ g).

Русский

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

LaTeX

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

Lean4

instance instIsScalarTower : IsScalarTower S (Module.End R M) (Module.End R M) :=
  ⟨smul_comp⟩

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