lift_comp_reindex_symm — Mathlib

English

The symmetric reindexing version yields the same relation with symmetrized arguments.

Русский

Симметричная переиндексация даёт ту же зависимость с симметризированными аргументами.

LaTeX

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

Lean4

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

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