domCoprod_domDomCongr_sumCongr — Mathlib

English

Naturality: applying domDomCongr to a domCoprod equals applying domCoprod to domDomCongr-reindexed factors.

Русский

Натуральность: применение domDomCongr к a domCoprod равно применению domCoprod к преобразованным по domDomCongr факторам.

LaTeX

$$$(a \mathrm{.domCoprod}\ b).\mathrm{domDomCongr}(\sigma_a\.sumCongr \sigma_b) = (a.\domDomCongr \sigma_a).\domCoprod (b.\domDomCongr \sigma_b).$$$

Lean4

/-- When passed an `Equiv.sumCongr`, `MultilinearMap.domDomCongr` distributes over
`MultilinearMap.domCoprod`. -/
theorem domCoprod_domDomCongr_sumCongr (a : MultilinearMap R (fun _ : ι₁ => N) N₁)
    (b : MultilinearMap R (fun _ : ι₂ => N) N₂) (σa : ι₁ ≃ ι₃) (σb : ι₂ ≃ ι₄) :
    (a.domCoprod b).domDomCongr (σa.sumCongr σb) = (a.domDomCongr σa).domCoprod (b.domDomCongr σb) :=
  rfl

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