Theorems · Theorem · functional analysis
InnerProductSpace.smul_left
∀ {𝕜 : Type u_4} {E : Type u_5} {inst : RCLike 𝕜} {inst_1 : SeminormedAddCommGroup E} [self : InnerProductSpace 𝕜 E]
(x y : E) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x yThe inner product is conjugate linear in the first coordinate.
- Defined in
- Mathlib.Analysis.InnerProductSpace.Defs
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 46 from the axioms · uses propext, Quot.sound
- Assumes
- InnerProductSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- RingHomstatement · cited by 10,189
- InnerProductSpacestatement and proof · cited by 3,523
- RCLikestatement and proof · cited by 2,829
- SeminormedAddCommGroupstatement and proof · cited by 2,671
- Inner.innerstatement · cited by 1,089
- starRingEndstatement · cited by 671
Cited by2
Results whose statement or proof uses this declaration.
- inner_smul_left_eq_star_smulproof · cited by 4
- PreInnerProductSpace.toCoreproof · cited by 2