codRestrict — Mathlib

English

The action of a scalar on a continuous alternating map corresponds to the scalar action on its associated continuous multilinear map.

Русский

Действие скаляра на непрерывном чередующемся отображении соответствует действию скаляра на сопутствующей непрерывной мультилинейной карте.

LaTeX

$$$\\forall c:\\, R' ,\\ f : \\mathrm{ContinuousAlternatingMap}(R,M,N,\\iota),\\ (c\\, f).toContinuousMultilinearMap = c \\cdot f.toContinuousMultilinearMap$$$

Lean4

/-- Restrict the codomain of a continuous alternating map to a submodule. -/
@[simps!]
def codRestrict (f : M [⋀^ι]→L[R] N) (p : Submodule R N) (h : ∀ v, f v ∈ p) : M [⋀^ι]→L[R] p :=
  { f.toAlternatingMap.codRestrict p h with toContinuousMultilinearMap := f.1.codRestrict p h }

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