Theorem DomMulAct.mk_smul_indicatorConstLp

Modification history

2024-07-09 22:38
Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean
feat(LpSpace/DomAct): add a lemma + `@[to_additive]` (#14488)
Added DomMulAct.mk_smul_indicatorConstLpView on Github →