domDomCongr_mul — Mathlib

English

Composing with a permutation of indices via a product of two permutations is equivalent to composing stepwise.

Русский

Композиция с перестановкой по индексу через произведение двух перестановок эквивалентна пошаговой композиции.

LaTeX

$$$ m.domDomCongr (σ₂ * σ₁) = (m.domDomCongr σ₁).domDomCongr σ₂ $$$

Lean4

theorem domDomCongr_mul (σ₁ : Equiv.Perm ι₁) (σ₂ : Equiv.Perm ι₁) (m : MultilinearMap R (fun _ : ι₁ => M₂) M₃) :
    m.domDomCongr (σ₂ * σ₁) = (m.domDomCongr σ₁).domDomCongr σ₂ :=
  rfl

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