# The quadratic form on a tensor product #

## Main definitions #

• QuadraticForm.tensorDistrib (Q₁ ⊗ₜ Q₂): the quadratic form on M₁ ⊗ M₂ constructed by applying Q₁ on M₁ and Q₂ on M₂. This construction is not available in characteristic two.
noncomputable def QuadraticForm.tensorDistrib (R : Type uR) (A : Type uA) {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [] :

The tensor product of two quadratic forms injects into quadratic forms on tensor products.

Note this is heterobasic; the quadratic form on the left can take values in a larger ring than the one on the right.

Instances For
@[simp]
theorem QuadraticForm.tensorDistrib_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [] (Q₁ : ) (Q₂ : ) (m₁ : M₁) (m₂ : M₂) :
↑(↑() (Q₁ ⊗ₜ[R] Q₂)) (m₁ ⊗ₜ[R] m₂) = Q₂ m₂ Q₁ m₁
@[inline, reducible]
noncomputable abbrev QuadraticForm.tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [] (Q₁ : ) (Q₂ : ) :

The tensor product of two quadratic forms, a shorthand for dot notation.

Instances For
theorem QuadraticForm.associated_tmul {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [] [] [] [] [Algebra R A] [Module R M₁] [Module A M₁] [SMulCommClass R A M₁] [IsScalarTower R A M₁] [Module R M₂] [] [] (Q₁ : ) (Q₂ : ) :