Theorems · Theorem · functional analysis

EuclideanSpace.inner_single_left

∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι) (a : 𝕜)
  (v : EuclideanSpace 𝕜 ι), inner 𝕜 (EuclideanSpace.single i a) v = (starRingEnd 𝕜) a * v.ofLp i

Defined in

Mathlib.Analysis.InnerProductSpace.PiL2

Cited by

3 results in Mathlib

Foundations

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

Assumes

RCLikeDecidableEqFintype