Namespace InnerProductSpace 1 theorems
- Averaging recovers a vector of a cyclic span
InnerProductSpace.exists_mem_norm_sub_lt_of_exists_mem_span_orbit_of_average0 below · cited by 1 · depth 17
InnerProductSpace 1 theoremsInnerProductSpace.exists_mem_norm_sub_lt_of_exists_mem_span_orbit_of_average 0 below · cited by 1 · depth 17