noncomputable def OrthonormalBasis.tensorProduct {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι₁ : Type u_4} {ι₂ : Type u_5} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : OrthonormalBasis (ι₁ × ι₂) 𝕜 (TensorProduct 𝕜 E F)

Equations

• b₁.tensorProduct b₂ = (b₁.toBasis.tensorProduct b₂.toBasis).toOrthonormalBasis ⋯

@[simp]

theorem OrthonormalBasis.tensorProduct_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι₁ : Type u_4} {ι₂ : Type u_5} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁) (j : ι₂) : (b₁.tensorProduct b₂) (i, j) = b₁ i ⊗ₜ[𝕜] b₂ j

theorem OrthonormalBasis.tensorProduct_apply' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι₁ : Type u_4} {ι₂ : Type u_5} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (i : ι₁ × ι₂) : (b₁.tensorProduct b₂) i = b₁ i.1 ⊗ₜ[𝕜] b₂ i.2

@[simp]

theorem OrthonormalBasis.tensorProduct_repr_tmul_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι₁ : Type u_4} {ι₂ : Type u_5} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : E) (y : F) (i : ι₁) (j : ι₂) : (b₁.tensorProduct b₂).repr (x ⊗ₜ[𝕜] y) (i, j) = b₁.repr x i * b₂.repr y j

theorem OrthonormalBasis.tensorProduct_repr_tmul_apply' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι₁ : Type u_4} {ι₂ : Type u_5} [Fintype ι₁] [Fintype ι₂] [DecidableEq ι₁] [DecidableEq ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : E) (y : F) (i : ι₁ × ι₂) : (b₁.tensorProduct b₂).repr (x ⊗ₜ[𝕜] y) i = b₁.repr x i.1 * b₂.repr y i.2