Theorem eq_of_norm_le_re_inner_eq_norm_sq

Modification history

2023-09-09 17:26
Mathlib/Analysis/InnerProductSpace/Basic.lean
feat: von Neumann Mean Ergodic Theorem (#6053)
Added eq_of_norm_le_re_inner_eq_norm_sqView on Github →