Normedtype 20260924 - #2112
Normedtype 20260924#2112affeldt-aist wants to merge 3 commits into
Conversation
20fe2c9 to
c2c904f
Compare
|
Here is the hierarchy graph for the first commit of this PR |
affeldt-aist
added
"bug" 🐛
…odule
- mv structures from tvs.v
- PseudoMetricNormedZmod inherits from TopologicalZmodule
- uniform{N,Z} now depends on topological{N,Z}
- structure of Uniform{N,Z}module for matrices (in `matrix_normedtype.v`)
- structure of metric space over products (in `metric_structure.v`)
- remove UniformLmodule
- product of {Topological,Uniform}{N,Z}Module
8dd5765 to
8aac8c5
Compare
How can I see the whole hierarchy graph for this PR ? |
Among the CI checks, click on "Generate HTML doc using Rocqnavi / generate-artifacts (pull_request)" Inside the list of steps, click on "Upload artifact" You'll find "Artifact download URL" with a URL to the Rocq navi documentation. (This has been set up by @yoshihiro503 and this is a great help.) |
| ### Removed | ||
|
|
||
| - in `tvs.v`: | ||
| + structure `PreUniformLmodule` |
There was a problem hiding this comment.
Why did you remove these structures ? Are they not necessary as joins for HB ? I'm under the impression that (Pre)UniformLmodule should still be included, inheriting from TopologicalLmodule and (Pre)UniformZmodule, and making ConvexTvs inherit from it. What do you think @affeldt-aist ?
There was a problem hiding this comment.
I removed UniformLmodule because (1) it was actually not used before this PR (no structure inherited from it) and (2) it was uninhabited (unless I am mistaken), making it look like dead code. Also, (3) I did have a version with convexTvsType inheriting from it but I was unable to inhabit the structure; I browsed the literature on TVSs but I couldn't convince myself that it is actually required, but I am not familiar with the theory, I may be wrong.
Maybe it was a join required by HB in the previous configuration but after the changes, at least, it is not required. (Note that TopologicalLmodule is still here.)
mkerjean
left a comment
mkerjean
left a comment
There was a problem hiding this comment.
This PR makes the UniformXmodules structures properly inherit from the TopologicalXmodule structures, and the ConvexTvsStructure inherit from UniformZmodule. I'm happy with this pull request, pending the clarification of the necessity of the UniformLmodule structure (see comment).
This branch has not been deployed
2 participants
Motivation for this change
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers