Skip to content

mv sequeeze for R earlier#2004

Open
affeldt-aist wants to merge 1 commit into
math-comp:masterfrom
affeldt-aist:metric_20260622
Open

mv sequeeze for R earlier#2004
affeldt-aist wants to merge 1 commit into
math-comp:masterfrom
affeldt-aist:metric_20260622

Conversation

@affeldt-aist

Copy link
Copy Markdown
Member
Motivation for this change

This PR is essentially moving squeeze_cvgr from normed_module.v to the topology_theory directory
so that it is available to develop the theory of TVSs.

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@affeldt-aist affeldt-aist requested a review from mkerjean June 23, 2026 07:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant