Theorems · Theorem · functional analysis

TensorProduct.inner_def

∀ {𝕜 : 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]
  (x y : TensorProduct 𝕜 E F),
  inner 𝕜 x y =
    (((TensorProduct.lift (TensorProduct.mapBilinear (RingHom.id 𝕜) E F 𝕜 𝕜)).compr₂ (LinearMap.mul' 𝕜 𝕜) ∘ₛₗ
          TensorProduct.map (innerₛₗ 𝕜) (innerₛₗ 𝕜))
        x)
      y

Defined in

Mathlib.Analysis.InnerProductSpace.TensorProduct

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceNormedAddCommGroupInnerProductSpace