Skip to content

feat(Algebra\ContinuedFractions): add partNums! and partDens!#39212

Open
emlis42 wants to merge 1 commit into
leanprover-community:masterfrom
emlis42:add-partD
Open

feat(Algebra\ContinuedFractions): add partNums! and partDens!#39212
emlis42 wants to merge 1 commit into
leanprover-community:masterfrom
emlis42:add-partD

Conversation

@emlis42
Copy link
Copy Markdown
Contributor

@emlis42 emlis42 commented May 11, 2026

This PR adds partNums! and partDens!, which provide infinite stream representations for the sequences of partial numerators and denominators of a generalized continued fraction.

@github-actions github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 11, 2026
@github-actions
Copy link
Copy Markdown

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@github-actions github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label May 11, 2026
@github-actions
Copy link
Copy Markdown

PR summary 6d6d92b454

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ partDens!
+ partNums!

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.


No changes to strong technical debt.
No changes to weak technical debt.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant