English
The multilinear map restricted to a subspace and then composed equals the restriction of the composition: (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.codRestrict p h).compMultilinearMap f = (g.compMultilinearMap f).codRestrict p (\lambda v. h (f v)). $$$$
Lean4
/-- An isomorphism of multilinear maps given an isomorphism between their codomains.
This is `LinearMap.compMultilinearMap` as an `S`-linear equivalence,
and the multilinear version of `LinearEquiv.congrRight`. -/
@[simps! apply symm_apply]
def _root_.LinearEquiv.multilinearMapCongrRight [LinearMap.CompatibleSMul M₂ M₃ S R]
[LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₂ ≃ₗ[R] M₃) : MultilinearMap R M₁ M₂ ≃ₗ[S] MultilinearMap R M₁ M₃
where
__ := g.toLinearMap.compMultilinearMapₗ S
invFun := g.symm.toLinearMap.compMultilinearMapₗ S
left_inv _ := by ext; simp
right_inv _ := by ext; simp
