English
Given a multilinear map f: M1 → M2 and a submodule p ⊆ M2 where f(v) ∈ p for all v, there is a unique multilinear map f: M1 → p that agrees with f on p.
Русский
Для отображения f: M1 → M2 и подмодуля p ⊆ M2, если f(v) ∈ p для всех v, существует единственная мультиленейная карта f: M1 → p, которая согласуется с f.
LaTeX
$$$\\text{codRestrict}(f,p,h) : MultilinearMap R M_1 p$ with $toFun(v)=f(v)$ and $h$ ensures $f(v) ∈ p$$$
Lean4
/-- Restrict the codomain of a multilinear map to a submodule.
This is the multilinear version of `LinearMap.codRestrict`. -/
@[simps]
def codRestrict (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ v, f v ∈ p) : MultilinearMap R M₁ p
where
toFun v := ⟨f v, h v⟩
map_update_add' _ _ _ _ := Subtype.ext <| MultilinearMap.map_update_add _ _ _ _ _
map_update_smul' _ _ _ _ := Subtype.ext <| MultilinearMap.map_update_smul _ _ _ _ _
