Theorems · Theorem · linear algebra

MultilinearMap.domDomCongr_apply

∀ {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}
  (σ : ι₁ ≃ ι₂) (m : MultilinearMap R (fun x => M₂) M₃) (v : ι₂ → M₂),
  (MultilinearMap.domDomCongr σ m) v = m fun i => v (σ i)

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModule