Skip to content

[Merged by Bors] - feat(SetTheory/Cardinal): formulas for sum (fun n : ℕ ↦ x ^ n)#32645

Closed
vihdzp wants to merge 5 commits intoleanprover-community:masterfrom
vihdzp:card
Closed

[Merged by Bors] - feat(SetTheory/Cardinal): formulas for sum (fun n : ℕ ↦ x ^ n)#32645
vihdzp wants to merge 5 commits intoleanprover-community:masterfrom
vihdzp:card

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Dec 9, 2025


Open in Gitpod

@vihdzp vihdzp changed the title feat: formulas for sum (fun n : ℕ ↦ x ^ n) feat(SetTheory/Cardinal): formulas for sum (fun n : ℕ ↦ x ^ n) Dec 9, 2025
@github-actions github-actions bot added the t-set-theory Set theory label Dec 9, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 9, 2025

PR summary 359769ac56

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ mk_list_eq_max
+ nonempty_out
+ sum_pow_eq_max_aleph0
+ sum_pow_le_max_aleph0
+ sum_zero_pow

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Comment thread Mathlib/SetTheory/Cardinal/Basic.lean Outdated
Co-authored-by: Artie Khovanov <artem.khovanov@gmail.com>
@vihdzp vihdzp requested a review from b-mehta December 21, 2025 18:32
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

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

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 22, 2025
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 22, 2025

Build failed (retrying...):

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 22, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(SetTheory/Cardinal): formulas for sum (fun n : ℕ ↦ x ^ n) [Merged by Bors] - feat(SetTheory/Cardinal): formulas for sum (fun n : ℕ ↦ x ^ n) Dec 22, 2025
@mathlib-bors mathlib-bors bot closed this Dec 22, 2025
@vihdzp vihdzp deleted the card branch March 13, 2026 22:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. t-set-theory Set theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants