restrictScalars_comp — Mathlib

English

Let f: N →ₗ[S] P and g: M →ₗ[S] N be linear maps with appropriate scalar actions. Then restricting scalars to R commutes with composition: (f ∘ g)|_R = f|_R ∘ g|_R.

Русский

Пусть f: N →ₗ[S] P и g: M →ₗ[S] N — линейные отображения; ограничение скаляров к R коммутирует с композицией: (f ∘ g)|_R = f|_R ∘ g|_R.

LaTeX

$$$ (f \circ g)|_{R} = (f|_{R}) \circ (g|_{R}) $$$

Lean4

@[simp]
theorem restrictScalars_comp [AddCommMonoid P] [Module S P] [Module R P] [CompatibleSMul N P R S]
    [CompatibleSMul M P R S] (f : N →ₗ[S] P) (g : M →ₗ[S] N) :
    (f ∘ₗ g).restrictScalars R = f.restrictScalars R ∘ₗ g.restrictScalars R :=
  rfl

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