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 #
The tensor product of two bilinear forms injects into bilinear forms on tensor products.
The tensor product of two bilinear forms, a shorthand for dot notation.
tensor_distrib as an equivalence.