Skip to content

Commit

Permalink
refactor(measure_theory/function/lp_space): split file (#19112)
Browse files Browse the repository at this point in the history 
This is the longest file that remains to port, and there is an obvious split to be made.
The new file is called `measure_theory.function/lp_seminorm`.

Other than the module docstrings, which have been tweaked to represent the split, the contents of the new file is moved without modification from the old one.
  • Loading branch information
@eric-wieser
eric-wieser committed May 27, 2023
1 parent 78fdf68 commit c4015ac
Show file tree
Hide file tree
Showing 2 changed files with 1,635 additions and 1,607 deletions.

0 comments on commit c4015ac

Please sign in to comment.