Theorems · Theorem · linear algebra

MultilinearMap.fromDirectSumEquiv_lof

∀ {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5}
  [inst : CommSemiring R] [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)]
  [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  [inst_5 : DecidableEq ι] [inst_6 : Finite ι] [inst_7 : (i : ι) → DecidableEq (κ i)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) M') (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
  ((MultilinearMap.fromDirectSumEquiv f) fun i => (DirectSum.lof R (κ i) (M i) (p i)) (x i)) = (f p) x

Defined in

Mathlib.LinearAlgebra.Multilinear.DirectSum

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleDecidableEqFiniteDecidableEq