Theorems · Theorem · functional analysis

OrthonormalBasis.toBasis_tensorProduct

∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] {ι₁ : Type u_6}
  {ι₂ : Type u_7} [inst_5 : Fintype ι₁] [inst_6 : Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E)
  (b₂ : OrthonormalBasis ι₂ 𝕜 F), (b₁.tensorProduct b₂).toBasis = b₁.toBasis.tensorProduct b₂.toBasis

Defined in

Mathlib.Analysis.InnerProductSpace.TensorProduct

Cited by

0 results in Mathlib

Foundations

Depth 248 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceNormedAddCommGroupInnerProductSpaceFintypeFintype