English
Auxiliary identity for iterated derivatives with a parametrized index set: a function equality between updates along different orders of indexing.
Русский
Вспомогательное соотношение для итеративной производной с параметризованным набором индексов: равенство функций при различном порядке обновления индексов.
LaTeX
$$$$ \text{iteratedFDeriv_aux}(s,e,m,a,z) = \text{corresponding updated version} $$$$
Lean4
/-- `MultilinearMap.domDomCongr` as a `LinearEquiv`. -/
@[simps apply symm_apply]
def domDomCongrLinearEquiv {ι₁ ι₂} (σ : ι₁ ≃ ι₂) :
MultilinearMap R (fun _ : ι₁ => M₂) M₃ ≃ₗ[S] MultilinearMap R (fun _ : ι₂ => M₂) M₃ :=
{ (domDomCongrEquiv σ : MultilinearMap R (fun _ : ι₁ => M₂) M₃ ≃+ MultilinearMap R (fun _ : ι₂ => M₂) M₃) with
map_smul' := fun c f => by
ext
simp [MultilinearMap.domDomCongr] }
