restrictScalars — Mathlib

English

If f is an A-multilinear map and A is an R-algebra with compatible actions, then f can be regarded as an R-multilinear map via the restriction of scalars.

Русский

Если f — A-мультиллинейное отображение, и A — алгебра над R с совместимыми действиями, то f можно рассматривать как R-мультилейное отображение через ограничение скаляров.

LaTeX

$$$\text{restrictScalars}: \text{ContinuousMultilinearMap } A M_1 M_2 \to \text{ContinuousMultilinearMap } R M_1 M_2.$$$

Lean4

/-- Reinterpret an `A`-multilinear map as an `R`-multilinear 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 : ContinuousMultilinearMap A M₁ M₂) : ContinuousMultilinearMap R M₁ M₂
    where
  toMultilinearMap := f.toMultilinearMap.restrictScalars R
  cont := f.cont

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