Skip to content

feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 4/5)#35316

Open
mkaratarakis wants to merge 15 commits intoleanprover-community:masterfrom
mkaratarakis:analysispart4
Open

feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 4/5)#35316
mkaratarakis wants to merge 15 commits intoleanprover-community:masterfrom
mkaratarakis:analysispart4

Conversation

@mkaratarakis
Copy link
Copy Markdown
Contributor

@mkaratarakis mkaratarakis commented Feb 14, 2026 •
edited
Loading

Open in Gitpod

@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 Feb 14, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 14, 2026

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.

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.

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
Copy link
Copy Markdown

github-actions bot commented Feb 14, 2026 •
edited
Loading

PR summary 96eec06566

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.NumberTheory.Transcendental.AnalyticPart (new file) 2499

Declarations diff

+ analyticOrderAt_deriv_eq_top_iff_of_eq_zero
+ analyticOrderAt_deriv_order_eq_succ
+ analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero
+ le_analyticOrderAt_iff_iteratedDeriv_eq_zero

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

@github-actions github-actions bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Feb 14, 2026
SnirBroshi
SnirBroshi reviewed Feb 14, 2026
View reviewed changes
@mathlib-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 18, 2026
@mkaratarakis mkaratarakis mentioned this pull request Feb 25, 2026
Open
3 tasks
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 10, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 10, 2026

This PR/issue depends on:

mkaratarakis and others added 11 commits March 16, 2026 18:47
@mkaratarakis
Merge branch 'master' into analysispart4
729f3ef
@mkaratarakis
Merge branch 'master' into analysispart4
0274bc9 
merge master
@mkaratarakis
Merge branch 'master' into analysispart4
846543f 
merge master
@mkaratarakis
Merge branch 'analysispart4' of https://github.com/mkaratarakis/mathlib4
19d6e7e 
 into analysispart4

pull
@mkaratarakis
Merge branch 'master' into analysispart4
f006fcc 
merge master
@mkaratarakis
Merge branch 'master' into analysispart4
5a5220e
@mkaratarakis
fix errors
ba7ef9a
@mkaratarakis
Merge branch 'analysispart4' of https://github.com/mkaratarakis/mathlib4
6df3bcd 
 into analysispart4
@mkaratarakis
mk all
e8a9205
@mkaratarakis
Merge branch 'master' into analysispart4
9e4240b
@mkaratarakis
Merge branch 'analysispart4' of https://github.com/mkaratarakis/mathlib4
c130f96 
 into analysispart4
MichaelStollBayreuth
MichaelStollBayreuth reviewed Mar 30, 2026
View reviewed changes
@MichaelStollBayreuth MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 30, 2026
@mkaratarakis
Copy link
Copy Markdown
Contributor Author

mkaratarakis commented Mar 31, 2026

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 31, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@MichaelStollBayreuth MichaelStollBayreuth MichaelStollBayreuth left review comments

+1 more reviewer

@SnirBroshi SnirBroshi SnirBroshi left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@MichaelStollBayreuth MichaelStollBayreuth

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mkaratarakis @SnirBroshi @MichaelStollBayreuth