smulRight_apply — Mathlib

English

If we scale coordinates indexed by a finite set s by c_i, then the multilinear map evaluates to the product of those c_i times the original value.

Русский

Если координаты, индексируемые конечным множеством s, масштабировать на c_i, то мультиленейное отображение принимает произведение c_i и исходного значения.

LaTeX

$$$$ f\bigl( s\text{.piecewise}(c_i \cdot m_i)\,m \bigr) = \Big(\prod_{i\in s} c_i\Big) f(m). $$$$

Lean4

@[simp]
theorem smulRight_apply (f : MultilinearMap R M₁ R) (z : M₂) (m : ∀ i, M₁ i) : f.smulRight z m = f m • z :=
  rfl

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