lift_comp_reindex — Mathlib

English

The lift of a multilinear map composed with reindexing equals the lift of the pulled-back map.

Русский

Лифт многочленного отображения в сочетании с переиндексацией равен лифту та же карта, вытянутая через обратное отображение.

LaTeX

$$$\\operatorname{lift} \\phi \\circ \\!\\!_{\\ell} (\\operatorname{reindex}_{R,s,e}) = \\operatorname{lift} \\bigl( (\\operatorname{domDomCongrLinearEquiv'}^{\\,-1}_{R,R,s,e} )\\phi \\bigr).$$$

Lean4

theorem lift_comp_reindex (e : ι ≃ ι₂) (φ : MultilinearMap R (fun i ↦ s (e.symm i)) E) :
    lift φ ∘ₗ (reindex R s e) = lift ((domDomCongrLinearEquiv' R R s _ e).symm φ) := by ext; simp [reindex]

Похожие утверждения