New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - split(analysis/normed/group/seminorm): Split off analysis.seminorm
#16152
Conversation
Are there any API changes? For the first move, you don't mention the name of the new file in the commit message. |
The only API change is
I can single it out to another PR if you ask. I was just impatient 😝 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
…16152) Move `group_seminorm` and `add_group_seminorm` to a new file `analysis.normed.group.seminorm`. Move `norm_add_group_seminorm` to `analysis.normed.group.basic`. Remove the `nonneg` field from `add_group_seminorm` and `group_seminorm` because it is redundant.
Pull request successfully merged into master. Build succeeded: |
analysis.seminorm
analysis.seminorm
Move
group_seminorm
andadd_group_seminorm
to a new fileanalysis.normed.group.seminorm
. Movenorm_add_group_seminorm
toanalysis.normed.group.basic
. Remove thenonneg
field fromadd_group_seminorm
andgroup_seminorm
because it is redundant.The goal is to rebase normed groups on seminorms. For this, we need to separate
add_group_seminorm
/group_seminorm
fromseminorm
becauseseminorm
depends onsemi_normed_ring
, which will eventually depend onadd_group_seminorm
.The folder organisation I am now aiming for is
analysis.normed
group
seminorm
: Group norms and seminorms as homomorphisms (the file here, but the norms are missing).basic
: Group norms and seminorms as classes (as it is today).ring
orfield
seminorm
: Ring norms and seminorms as homomorphisms (as is being added in [Merged by Bors] - feat(analysis/normed/ring/seminorm): add ring_seminorm, ring_norm #14115).basic
: Ring norms and seminorms as classes (as it is today.module
orspace
seminorm
: Module norms and seminorms as homomorphisms (as it is inanalysis.seminorm
today, but the norms are missing).basic
: Ring norms and seminorms as classes (as it is inanalysis.normed_space.basic
today).Every time, the
.basic
file would import the.seminorm
file, rather than the other way around.Zulip