Orthonormal Bases of Tensor Products #
Compatibility module for the upstream Monlib4 file. The old declarations in this file,
including OrthonormalBasis.tensorProduct and its simp lemmas, are already available
from current Mathlib through the imports above.
theorem
Basis.tensorProduct_repr_tmul_apply'
{R : Type u_1}
{S : Type u_2}
{M : Type u_3}
{N : Type u_4}
{ι : Type u_5}
{κ : Type u_6}
[CommSemiring R]
[Semiring S]
[Algebra R S]
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
[AddCommMonoid N]
[Module R N]
(b : Module.Basis ι S M)
(c : Module.Basis κ R N)
(m : M)
(n : N)
(i : ι × κ)
: