domDomCongr_trans — Mathlib

English

The operation of applying domain-domains congruence via an equivalence σ between index sets is itself organized into an equivalence of multilinear maps.

Русский

Операция применения домена-доменного преобразования через эквивалентность σ между индексными множествами образует эквивалентность мультиленейных карт.

LaTeX

$$@[simps apply] def domDomCongrEquiv (σ) : MultilinearMap R (fun _ : ι₁ => M₂) M₃ ≃+ MultilinearMap R (fun _ : ι₂ => M₂) M₃$$

Lean4

theorem domDomCongr_trans (σ₁ : ι₁ ≃ ι₂) (σ₂ : ι₂ ≃ ι₃) (m : MultilinearMap R (fun _ : ι₁ => M₂) M₃) :
    m.domDomCongr (σ₁.trans σ₂) = (m.domDomCongr σ₁).domDomCongr σ₂ :=
  rfl

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