Theorems · Definition · linear algebra

MultilinearMap.domDomCongr

{R : Type uR} →
  {M₂ : Type v₂} →
    {M₃ : Type v₃} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : AddCommMonoid M₃] →
            [inst_3 : Module R M₂] →
              [inst_4 : Module R M₃] →
                {ι₁ : Type u_1} →
                  {ι₂ : Type u_2} → ι₁ ≃ ι₂ → MultilinearMap R (fun x => M₂) M₃ → MultilinearMap R (fun x => M₂) M₃

Transfer the arguments to a map along an equivalence between argument indices. The naming is derived from Finsupp.domCongr, noting that here the permutation applies to the domain of the domain.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

20 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModule