Theorem RCLike.linearIndependent_of_ne_zero_of_wInner_one_eq_zero

Modification history

2024-10-11 13:11
Mathlib/Analysis/RCLike/Inner.lean
feat: L2 inner product of finite sequences (#16447) …
Added RCLike.linearIndependent_of_ne_zero_of_wInner_one_eq_zeroView on Github →