Skip to content
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.

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

[Merged by Bors] - feat(RingTheory/PowerSeries/WellKnown): the power series of 1 / ((1 - x) ^ (d + 1)) with coefficients in a commutative ring S, where d : ℕ. #11255

Closed
wants to merge 12 commits into from

Conversation

FMLJohn
Copy link
Collaborator

@FMLJohn FMLJohn commented Mar 8, 2024


Open in Gitpod

Mathlib/RingTheory/PowerSeries/Inverse.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
@FMLJohn
Copy link
Collaborator Author

FMLJohn commented Mar 8, 2024

The main content of this pull request is: creating a definition invOneSubPow such that for any commutative ring S and natural number d, invOneSubPow d : S⟦X⟧ˣ has value mk fun n => Nat.choose (d + n) d and inverse (1 - X) ^ (d + 1).

@kbuzzard @urkud @jcommelin @ChrisHughes24 @jjaassoonn

@FMLJohn FMLJohn added the t-algebra Algebra (groups, rings, fields, etc) label Mar 8, 2024
Mathlib/Data/Nat/Choose/Sum.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/Inverse.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
@fpvandoorn
Copy link
Member

please mark as awaiting-review if it's ready for review

@FMLJohn
Copy link
Collaborator Author

FMLJohn commented Apr 8, 2024

please mark as awaiting-review if it's ready for review

Recently I have come up with an idea to change the contents of this pull request significantly. I will mark it as awaiting-review after I have made the change.

@fpvandoorn fpvandoorn added the awaiting-author A reviewer has asked the author a question or requested changes label Apr 8, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 17, 2024
@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 Apr 27, 2024
@FMLJohn FMLJohn changed the title feat(RingTheory/PowerSeries/WellKnown): the power series of 1 / ((1 - x) ^ (d + 1)) with coefficients in a field k, where d : ℕ. feat(RingTheory/PowerSeries/WellKnown): the power series of 1 / ((1 - x) ^ (d + 1)) with coefficients in a commutative ring S, where d : ℕ. Apr 27, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 27, 2024
@FMLJohn FMLJohn added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 27, 2024
@FMLJohn FMLJohn requested a review from kbuzzard May 3, 2024 13:19
Copy link
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

Sorry I took so long to get around to this.

Mathlib/Data/Nat/Choose/Sum.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
@kbuzzard kbuzzard added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels May 9, 2024
@kbuzzard kbuzzard self-assigned this May 9, 2024
@FMLJohn FMLJohn added awaiting-CI awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI labels May 10, 2024
Copy link
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

This is fine now. I've left some minor golfy comments; please fix them before merging!

bors d+

Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/PowerSeries/WellKnown.lean Outdated Show resolved Hide resolved
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 16, 2024

✌️ FMLJohn can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@FMLJohn
Copy link
Collaborator Author

FMLJohn commented May 16, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request May 16, 2024
…- x) ^ (d + 1))` with coefficients in a commutative ring `S`, where `d : ℕ`. (#11255)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 16, 2024

Build failed:

@FMLJohn
Copy link
Collaborator Author

FMLJohn commented May 16, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request May 16, 2024
…- x) ^ (d + 1))` with coefficients in a commutative ring `S`, where `d : ℕ`. (#11255)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 16, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/PowerSeries/WellKnown): the power series of 1 / ((1 - x) ^ (d + 1)) with coefficients in a commutative ring S, where d : ℕ. [Merged by Bors] - feat(RingTheory/PowerSeries/WellKnown): the power series of 1 / ((1 - x) ^ (d + 1)) with coefficients in a commutative ring S, where d : ℕ. May 16, 2024
@mathlib-bors mathlib-bors bot closed this May 16, 2024
@mathlib-bors mathlib-bors bot deleted the one_sub_pow_inv branch May 16, 2024 21:29
grunweg pushed a commit that referenced this pull request May 17, 2024
…- x) ^ (d + 1))` with coefficients in a commutative ring `S`, where `d : ℕ`. (#11255)
callesonne pushed a commit that referenced this pull request Jun 4, 2024
…- x) ^ (d + 1))` with coefficients in a commutative ring `S`, where `d : ℕ`. (#11255)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated 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.

5 participants