English
Definition of iteratedFDerivComponent: a multilinear map constructed by restricting f to a subset s and using a bijection e to permute coordinates, preserving multilinearity in the remaining coordinates.
Русский
Определение iteratedFDerivComponent: многолинейная карта, построенная ограничением f на подмножество s и использованием биекции e для перестановки координат, сохраняя многолинейность в оставшихся координатах.
LaTeX
$$$\text{iteratedFDerivComponent} : \text{MultilinearMap} \; (M_1) \; (M_2) \rightarrow \text{MultilinearMap} \; (M_1')$$$
Lean4
/-- An isomorphism of multilinear maps given an isomorphism between their domains.
This is `MultilinearMap.compLinearMap` as a linear equivalence,
and the multilinear version of `LinearEquiv.congrLeft`. -/
@[simps! apply symm_apply]
def _root_.LinearEquiv.multilinearMapCongrLeft (e : Π (i : ι), M₁ i ≃ₗ[R] M₁' i) :
(MultilinearMap R M₁' M₂) ≃ₗ[R] MultilinearMap R M₁ M₂
where
__ := compLinearMapₗ (e · |>.toLinearMap)
invFun := compLinearMapₗ (e · |>.symm.toLinearMap)
left_inv _ := by ext; simp
right_inv _ := by ext; simp
