# mathlib3documentation

linear_algebra.bilinear_form.tensor_product

# The bilinear form on a tensor product #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main definitions #

• bilin_form.tensor_distrib (B₁ ⊗ₜ B₂): the bilinear form on M₁ ⊗ M₂ constructed by applying B₁ on M₁ and B₂ on M₂.
• bilin_form.tensor_distrib_equiv: bilin_form.tensor_distrib as an equivalence on finite free modules.
def bilin_form.tensor_distrib {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] :
M₁) M₂) →ₗ[R] M₁ M₂)

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

Equations
@[simp]
theorem bilin_form.tensor_distrib_tmul {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (B₁ : M₁) (B₂ : M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) :
(bilin_form.tensor_distrib (B₁ ⊗ₜ[R] B₂)) (m₁ ⊗ₜ[R] m₂) (m₁' ⊗ₜ[R] m₂') = B₁ m₁ m₁' * B₂ m₂ m₂'
@[protected, reducible]
def bilin_form.tmul {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [add_comm_monoid M₁] [add_comm_monoid M₂] [ M₁] [ M₂] (B₁ : M₁) (B₂ : M₂) :
M₁ M₂)

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

Equations
noncomputable def bilin_form.tensor_distrib_equiv {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [comm_ring R] [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] [ M₁] [ M₁] [ M₂] [ M₂] [nontrivial R] :
M₁) M₂) ≃ₗ[R] M₁ M₂)

tensor_distrib as an equivalence.

Equations
@[simp]
theorem bilin_form.tensor_distrib_equiv_apply {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [comm_ring R] [add_comm_group M₁] [add_comm_group M₂] [ M₁] [ M₂] [ M₁] [ M₁] [ M₂] [ M₂] [nontrivial R] (B : M₁) M₂)) :