Theorems · Theorem · linear algebra

PiTensorProduct.lift_comp_reindex_symm

∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E]
  [inst_4 : Module R E] (e : ι ≃ ι₂) (φ : MultilinearMap R s E),
  PiTensorProduct.lift φ ∘ₗ ↑(PiTensorProduct.reindex R s e).symm =
    PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e) φ)

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModule