Theorem RCLike.wInner_one_eq_sum

Modification history

2025-05-03 01:57

Mathlib/Analysis/RCLike/Inner.lean

chore(Analysis/InnerProductSpace): make `𝕜` an explicit argument of `inner` (#24499) …

Modified RCLike.wInner_one_eq_sum View on Github →

2024-10-11 13:11

Mathlib/Analysis/RCLike/Inner.lean

feat: L2 inner product of finite sequences (#16447) …

Added RCLike.wInner_one_eq_sum View on Github →