instModuleOfSMulCommClassOfContinuousConstSMul

English

The combined additive structure commutes with the coercion to functions: the map of sums matches the sum of maps at the function level.

Русский

Суммирование отображений совместимо с переходом к функциям: отображение суммы эквивалентно сумме отображений на уровне функций.

LaTeX

$$$\big( f+g \big)^{\sim} = f^{\sim} + g^{\sim}$$$

Lean4

instance [Semiring S] [Module S W] [SMulCommClass R S W] [ContinuousConstSMul S W] : Module S (P →ᴬ[R] W) :=
  Function.Injective.module S ⟨⟨fun f ↦ f.toAffineMap.toFun, rfl⟩, coe_add⟩ coe_injective coe_smul

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