Theorem inner_smul_left_eq_smul

Modification history

2024-10-05 09:45
Mathlib/Analysis/InnerProductSpace/Basic.lean
refactor: generalise linearity of inner product (#17384) …
Added inner_smul_left_eq_smulView on Github →