Theorems · Theorem · linear algebra

PiTensorProduct.ext

∀ {ι : Type u_1} {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]
  {φ₁ φ₂ : (PiTensorProduct R fun i => s i) →ₗ[R] E},
  φ₁.compMultilinearMap (PiTensorProduct.tprod R) = φ₂.compMultilinearMap (PiTensorProduct.tprod R) → φ₁ = φ₂

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

26 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModule