Skip to content

Conversation

@t6s
Copy link
Member

@t6s t6s commented Nov 15, 2024

Motivation for this change

There are several lemmas for series stated with zero-based indexing
0 <= k < n and n <oo.
This PR generalizes them to m <= k < n and m <= n<oo.

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

Reference: How to document

Reminder to reviewers

@t6s
Copy link
Member Author

t6s commented Nov 15, 2024

Two lemmas for orderTypes are added in mathcomp_extra.v too.

@t6s t6s requested a review from affeldt-aist November 15, 2024 01:51
Copy link
Member

@affeldt-aist affeldt-aist left a comment

Choose a reason for hiding this comment

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

Excellent! No doubt it will be useful at some point. Just need a rebase for the changelog.

@affeldt-aist
Copy link
Member

@t6s do you have more changes to commit?

@t6s
Copy link
Member Author

t6s commented Jan 7, 2025

@t6s do you have more changes to commit?

Not for now.
There are points that can be further generalized, but it will take more time than I expected.
I will rather do that as a separate PR.

@affeldt-aist
Copy link
Member

Let's merge then!

@affeldt-aist affeldt-aist added this to the 1.9.0 milestone Jan 7, 2025
@affeldt-aist affeldt-aist added the renaming/refactoring 🔧 This is about a renaming or refactoring in the library label Jan 7, 2025
@affeldt-aist affeldt-aist merged commit 4fced68 into math-comp:master Jan 7, 2025
31 of 32 checks passed
ndslusarz pushed a commit to ndslusarz/analysis that referenced this pull request Feb 12, 2025
* generalize some lemmas for series

---------

Co-authored-by: Reynald Affeldt <[email protected]>
@t6s t6s deleted the gen_seq branch August 13, 2025 17:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

renaming/refactoring 🔧 This is about a renaming or refactoring in the library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants