Theorems · Theorem · functional analysis

InnerProductSpace.symm_toEuclideanLin_rankOne

∀ {𝕜 : Type u_7} {m : Type u_8} {n : Type u_9} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (x : EuclideanSpace 𝕜 m) (y : EuclideanSpace 𝕜 n),
  Matrix.toEuclideanLin.symm ↑(((InnerProductSpace.rankOne 𝕜) x) y) = Matrix.vecMulVec x.ofLp (star y.ofLp)

Defined in: Mathlib.Analysis.InnerProductSpace.PiL2
Cited by: 1 results in Mathlib
Foundations: Depth 228 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: RCLike Fintype Fintype DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites29

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
RingHom.idstatement · cited by 18,349
LinearMapstatement · cited by 10,215
ENNRealstatement · cited by 9,879
Fintypestatement and proof · cited by 7,736
ContinuousLinearMapstatement · cited by 5,352
Matrixstatement · cited by 4,303
LinearEquivstatement · cited by 3,317
one_mulproof · cited by 2,841
RCLikestatement and proof · cited by 2,829
mul_commproof · cited by 2,262
LinearEquiv.symmstatement and proof · cited by 1,461

Cited by1

Results whose statement or proof uses this declaration.

Matrix.posSemidef_iff_eq_sum_vecMulVecproof · cited by 0