Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measure_theory.integrable.inner_const

Modification history

2023-05-15 16:30
src/measure_theory/function/l1_space.lean
chore(measure_theory/{integral/set_integral,function/*}): split out inner product space material (#19019) …
Modified measure_theory.integrable.inner_constView on Github →
2021-08-12 15:02
src/measure_theory/function/l1_space.lean
feat(measure_theory/lp_space): add mem_Lp and integrable lemmas for is_R_or_C.re/im and inner product with a constant (#8615)
Added measure_theory.integrable.inner_constView on Github →