Theorems · Theorem · number theory

QuadraticMap.associated_tmul

∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} {N₁ : Type uN₁} {N₂ : Type uN₂} [inst : CommRing R]
  [inst_1 : CommRing A] [inst_2 : AddCommGroup M₁] [inst_3 : AddCommGroup M₂] [inst_4 : AddCommGroup N₁]
  [inst_5 : AddCommGroup 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 : IsScalarTower R A N₁] [inst_14 : Module R M₂] [inst_15 : Module R N₂] [inst_16 : Invertible 2]
  [inst_17 : Invertible 2] (Q₁ : QuadraticMap A M₁ N₁) (Q₂ : QuadraticMap R M₂ N₂),
  QuadraticMap.associated (Q₁.tmul Q₂) = (QuadraticMap.associated Q₁).tmul (QuadraticMap.associated Q₂)

Defined in

Mathlib.LinearAlgebra.QuadraticForm.TensorProduct

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAddCommGroupAddCommGroupAddCommGroupAddCommGroupAlgebraModuleModuleModuleModuleSMulCommClassIsScalarTowerIsScalarTowerModuleModuleInvertibleInvertible