restrictScalars — Mathlib

English

If c: ι → R and m: ι → M, and s is a Finset, then f on the piecewise c_i • m_i is equal to the product of c_i over i in s times f on m.

Русский

Если c: ι → R, m: ι → M и s — Finset, то f на кусочно-определенном по c_i • m_i равно произведению c_i по i в s, умноженное на f на m.

LaTeX

$$$ f( s.piecewise (c \circ m) m ) = (\prod_{i \in s} c_i) \cdot f(m). $$$

Lean4

/-- Reinterpret a continuous `A`-alternating map as a continuous `R`-alternating map, if `A` is an
algebra over `R` and their actions on all involved modules agree with the action of `R` on `A`. -/
def restrictScalars (f : M [⋀^ι]→L[A] N) : M [⋀^ι]→L[R] N :=
  { f with toContinuousMultilinearMap := f.1.restrictScalars R }

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