Theorem MeasureTheory.L2.real_inner_indicatorConstLp_one_indicatorConstLp_one

Modification history

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