Skip to content

port of classical from lspace_master #1598

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.

Sign up for GitHub

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

Jump to bottom
Merged
affeldt-aist merged 1 commit into from
Apr 30, 2025
Merged

port of classical from lspace_master #1598

affeldt-aist merged 1 commit into from
Apr 30, 2025
+82 −0

Conversation

@hoheinzollern
Copy link
Member

@hoheinzollern hoheinzollern commented Apr 30, 2025 •
edited
Loading

Motivation for this change

This is part of the split of PR #1506 introducing Lp-spaces.
This PR adds lemmas to classical that are necessary additions.

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

@hoheinzollern @affeldt-aist
@CohenCyril @proux01
Port of lemmas in classical from lspace master
152d4b5 
Co-authored-by: Reynald Affeldt <[email protected]>
Co-authored-by: Cyril Cohen <[email protected]>
Co-authored-by: Pierre Roux <[email protected]>
@affeldt-aist affeldt-aist self-requested a review April 30, 2025 06:56
affeldt-aist
affeldt-aist approved these changes Apr 30, 2025
View reviewed changes
Copy link
Member

@affeldt-aist affeldt-aist left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK (the change of Arguments for subset_set{1,2} is not documented but that's maybe fine).

@affeldt-aist affeldt-aist merged commit f7fbb86 into math-comp:master Apr 30, 2025
32 of 35 checks passed
IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this pull request Jun 20, 2025
@hoheinzollern @affeldt-aist
@CohenCyril @proux01 @t6s @IshiguroYoshihiro
Port of lemmas in classical from lspace master (math-comp#1598)`
9c1c87b 
Co-authored-by: Reynald Affeldt <[email protected]>
Co-authored-by: Cyril Cohen <[email protected]>
Co-authored-by: Pierre Roux <[email protected]>
Co-authored-by: Takafumi Saikawa <[email protected]>
@hoheinzollern hoheinzollern mentioned this pull request Jul 8, 2025
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@affeldt-aist affeldt-aist affeldt-aist approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@hoheinzollern @affeldt-aist