compMultilinearMap_domDomCongr — Mathlib

English

The nested composition identity: (g.comp g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f).

Русский

Вложенная композиция: (g.comp g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f).

LaTeX

$$$$ (g.comp g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f). $$$$

Lean4

@[simp]
theorem compMultilinearMap_domDomCongr (σ : ι₁ ≃ ι₂) (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R (fun _ : ι₁ => M') M₂) :
    (g.compMultilinearMap f).domDomCongr σ = g.compMultilinearMap (f.domDomCongr σ) :=
  by
  ext
  simp [MultilinearMap.domDomCongr]

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