[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 : ℕ.
#53688
FMLJohndetect_sha_changes.yml
on: pull_request
Add annotations
2m 53s
Annotations
1 warning and 3 notices
|
Add annotations
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/setup-python@v4. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
Synchronization:
Mathlib/Data/Real/NNReal.lean#L15
See review instructions and diff at
https://leanprover-community.github.io/mathlib-port-status/file/data/real/nnreal?range=de29c328903507bb7aff506af9135f4bdaf1849c..b1abe23ae96fef89ad30d9f4362c307f72a55010
|
|
Synchronization:
Mathlib/SetTheory/Game/Basic.lean#L10
See review instructions and diff at
https://leanprover-community.github.io/mathlib-port-status/file/set_theory/game/basic?range=6623e6af705e97002a9054c1c05a980180276fc1..8900d545017cd21961daa2a1734bb658ef52c618
|
|
Synchronization:
Mathlib/SetTheory/Surreal/Basic.lean#L9
See review instructions and diff at
https://leanprover-community.github.io/mathlib-port-status/file/set_theory/surreal/basic?range=ee02a30e209a2a77b93eac1254e8c66e76192f54..8900d545017cd21961daa2a1734bb658ef52c618
|