Theorem MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp

Modification history

2025-10-11 15:08
Mathlib/MeasureTheory/Function/L2Space.lean
feat: introduce Gram matrices (#25883) …
Added MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLpView on Github →