Theorems · Theorem · number theory

QuadraticForm.tmul_tensorMap_apply

∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup M₃] [inst_4 : AddCommGroup M₄]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] [inst_9 : Invertible 2]
  {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄}
  (f : Q₁ →qᵢ Q₂) (g : Q₃ →qᵢ Q₄) (x : TensorProduct R M₁ M₃),
  (Q₂.tmul Q₄) ((TensorProduct.map f.toLinearMap g.toLinearMap) x) = (Q₁.tmul Q₃) x

Defined in

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupAddCommGroupAddCommGroupModuleModuleModuleModuleInvertible