smul_apply — Mathlib

English

The scalar action on ContinuousMultilinearMap is compatible with the scalar actions from two rings R' and R'' forming a scalar tower: (R',R'')-SMul on CMMap respects the tower property.

Русский

Действие скаляров из двух колец образует тензорную башню: совместимость действий скаляров сохраняется.

LaTeX

$$$\\text{IsScalarTower}(R',R'',\\mathrm{ContinuousMultilinearMap}(A,M_1,M_2)).$$$

Lean4

@[simp]
theorem smul_apply (f : ContinuousMultilinearMap A M₁ M₂) (c : R') (m : ∀ i, M₁ i) : (c • f) m = c • f m :=
  rfl

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