Skip to content

Commit

Permalink
chore(measure_theory/integral): split up measure_theory.integral.lebe…
Browse files Browse the repository at this point in the history 
…sgue (#18904)

This PR shortens the 3056-line-long file `measure_theory.integral.lebesgue`, by removing a 1000-line initial segment into a new file `measure_theory.function.simple_func`.
  • Loading branch information
@loefflerd
loefflerd committed May 1, 2023
1 parent d20a8cd commit 7317149
Show file tree
Hide file tree
Showing 4 changed files with 1,023 additions and 997 deletions.

0 comments on commit 7317149

Please sign in to comment.