Theorems · Theorem · linear algebra

InnerProductSpace.canonicalCovariantTensor_eq_sum

∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {ι : Type u_2} [inst_3 : Fintype ι] (v : OrthonormalBasis ι ℝ E),
  InnerProductSpace.canonicalCovariantTensor E = ∑ i, v i ⊗ₜ[ℝ] v i

Representation of the canonical covariant tensor in terms of an orthonormal basis.

Defined in

Mathlib.Analysis.InnerProductSpace.CanonicalTensor

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFiniteDimensionalFintype