mathlib3
chore(measure_theory/bochner_integration): make proofs shorter
#1871

Merged

chore(measure_theory/bochner_integration): make proofs shorter #1871

mergify merged 5 commits into leanprover-community:master from aceg00:remove_pos_part

More consistent use of the dot notation

854a499a

Revert "More consistent use of the dot notation"

57aaf226

Revert "Revert "More consistent use of the dot notation""

9202301c

sgouezel commented on 2020-01-11

fix things

bf7e167d

sgouezel approved these changes on 2020-01-11

sgouezel added ready-to-merge

Merge branch 'master' into remove_pos_part

2d0a0df4

mergify merged 25dded2d into master 6 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone