Theorems · Theorem · linear algebra

Basis.multilinearMap_apply

∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {M : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {κ : ι → Type u_5} (b : (i : ι) → Module.Basis (κ i) R (M i)) {ι' : Type u_6}
  {N : Type u_7} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (b' : Module.Basis ι' R N) [inst_5 : Fintype ι]
  [inst_6 : ∀ (i : ι), Finite (κ i)] (i : ((i : ι) → κ i) × ι'),
  (Basis.multilinearMap b b') i =
    (LinearMap.id.smulRight (b' i.2)).compMultilinearMap
      ((MultilinearMap.mkPiRing R ι 1).compLinearMap fun i' => (b i').coord (i.1 i'))

Defined in

Mathlib.LinearAlgebra.Multilinear.Basis

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleFintypeFinite