English
Restricting the codomain and composing with a multilinear map corresponds to restricting the composition to the codomain restriction: (g.codRestrict p h).compMultilinearMap f = (g.compMultilinearMap f).codRestrict p (λ v, h (f v)).
Русский
Ограничение кодом и композиция с мультиленейным отображением соответствуют ограничению композиции по кодомаппингу: (g.codRestrict p h).compMultilinearMap f = (g.compMultilinearMap f).codRestrict p (λ v, h (f v)).
LaTeX
$$$$ (g\text{.codRestrict } p h).compMultilinearMap f = (g.compMultilinearMap f).codRestrict p (\lambda v. h (f v)). $$$$
Lean4
/-- The multilinear version of `LinearMap.comp_codRestrict` -/
@[simp]
theorem compMultilinearMap_codRestrict (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) (p : Submodule R M₃) (h) :
(g.codRestrict p h).compMultilinearMap f = (g.compMultilinearMap f).codRestrict p fun v => h (f v) :=
rfl
