Skip to content

Commit

Permalink
refactor(analysis/normed_space/basic): split into normed_space and ..…
Browse files Browse the repository at this point in the history 
…/normed/normed_field (#12410)

Splits off the sections about normed rings and fields of the file `analysis/normed_space/basic` into a new file `analysis/normed/normed_field`.
  • Loading branch information
@mcdoll
mcdoll committed Mar 2, 2022
1 parent 423328e commit ce26d75
Show file tree
Hide file tree
Showing 2 changed files with 673 additions and 655 deletions.

0 comments on commit ce26d75

Please sign in to comment.