Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-08-10 18:08
3b279c17
View on Github →
feat(measure_theory/l2_space): generalize inner_indicator_const_Lp_one from R to is_R_or_C (
#8602
)
Estimated changes
Modified
src/measure_theory/l2_space.lean
modified
theorem
measure_theory.L2.inner_indicator_const_Lp_one