Theorems · Theorem · linear algebra

LinearMap.BilinMap.tmul_isSymm

∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N₁]
  [inst_5 : AddCommMonoid N₂] [inst_6 : Algebra R A] [inst_7 : Module R M₁] [inst_8 : Module A M₁]
  [inst_9 : Module R N₁] [inst_10 : Module A N₁] [inst_11 : SMulCommClass R A M₁] [inst_12 : IsScalarTower R A M₁]
  [inst_13 : SMulCommClass R A N₁] [inst_14 : IsScalarTower R A N₁] [inst_15 : Module R M₂] [inst_16 : Module R N₂]
  {B₁ : LinearMap.BilinMap A M₁ N₁} {B₂ : LinearMap.BilinMap R M₂ N₂},
  (∀ (x y : M₁), (B₁ x) y = (B₁ y) x) →
    (∀ (x y : M₂), (B₂ x) y = (B₂ y) x) → ∀ (x y : TensorProduct R M₁ M₂), ((B₁.tmul B₂) x) y = ((B₁.tmul B₂) y) x

A tensor product of symmetric bilinear maps is symmetric.

Defined in

Mathlib.LinearAlgebra.BilinearForm.TensorProduct

Cited by

2 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringAddCommMonoidAddCommMonoidAddCommMonoidAddCommMonoidAlgebraModuleModuleModuleModuleSMulCommClassIsScalarTowerSMulCommClassIsScalarTowerModuleModule