map_smul_univ — Mathlib

English

In the setting of a Pi-algebra, the action of mkPiAlgebra on a family m: ι → A simply equals the product ∏ i∈ι m_i.

Русский

В настройке Pi-алгебры действие mkPiAlgebra на семейство m: ι → A равно произведению ∏_{i} m_i.

LaTeX

$$$\\operatorname{mkPiAlgebra} \\; R\\ ι\\ A\\ m = \\prod i \\; m_i.$$$

Lean4

/-- Multiplicativity of a multilinear map along all coordinates at the same time,
writing `f (fun i => c i • m i)` as `(∏ i, c i) • f m`. -/
theorem map_smul_univ [Fintype ι] (c : ι → R) (m : ∀ i, M₁ i) : (f fun i => c i • m i) = (∏ i, c i) • f m := by
  classical simpa using map_piecewise_smul f c m Finset.univ

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