lebesgue): use `‖a‖₊ •` instead of `ennreal.of_real (|a|) *`
#19018

Open

refactor(measure_theory/measure/lebesgue): use `‖a‖₊ •` instead of `ennreal.of_real (|a|) *` #19018

eric-wieser wants to merge 6 commits into master from eric-wieser/nnnorm-smul

wip

bc0f9e3a

wip

78101ac8

Merge remote-tracking branch 'origin/master' into eric-wieser/nnnorm-…

b7c4c646

eric-wieser added WIP

eric-wieser added awaiting-CI

eric-wieser requested a review 2 years ago

github-actions added modifies-synchronized-file

fix

8ef9630a

fix

2f781bf6

Merge remote-tracking branch 'origin/master' into eric-wieser/nnnorm-…

ddaea51a

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

WIP awaiting-CI modifies-synchronized-file too-late

Milestone

No milestone