Theorems · Theorem · number theory

QuadraticForm.tensorDistrib_tmul

∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : AddCommGroup M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂]
  [inst_10 : Invertible 2] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂),
  ((QuadraticForm.tensorDistrib R A) (Q₁ ⊗ₜ[R] Q₂)) (m₁ ⊗ₜ[R] m₂) = Q₂ m₂ • Q₁ m₁

Defined in

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAddCommGroupAddCommGroupAlgebraModuleModuleSMulCommClassIsScalarTowerModuleInvertible