Theorems · Theorem · functional analysis

PreInnerProductSpace.Core.smul_left

∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  (self : PreInnerProductSpace.Core 𝕜 F) (x y : F) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y

The inner product is conjugate linear in the first coordinate.

Defined in

Mathlib.Analysis.InnerProductSpace.Defs

Cited by

1 results in Mathlib

Foundations

Depth 47 from the axioms · uses propext, Quot.sound

Assumes

RCLikeAddCommGroupModule