Skip to content

[Merged by Bors] - feat(Mathlib/FieldTheory): define differential fields#14860

Closed
Command-Master wants to merge 58 commits intomasterfrom
CommandMaster_DifferentialField
Closed

[Merged by Bors] - feat(Mathlib/FieldTheory): define differential fields#14860
Command-Master wants to merge 58 commits intomasterfrom
CommandMaster_DifferentialField

Conversation

@Command-Master
Copy link
Copy Markdown
Collaborator

@Command-Master Command-Master commented Jul 18, 2024 •
edited
Loading

Command-Master and others added 20 commits July 13, 2024 07:43
@Command-Master
Add bundled differential rings and algberas
f5ecd0d
@Command-Master
increase synth instance time
7d35fb3
@Command-Master
Export deriv_algebraMap
fd308f9
@Command-Master
Move file
71f6141
@Command-Master
golf
6e65f24
@Command-Master @erdOne
Apply suggestions from code review
80919b1 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@Command-Master
Test
4147685
@Command-Master
Merge branch 'CommandMaster_diffring' into CommandMaster_Differential…
c19d296 
…Field
@Command-Master
deffile
6041ea0
@Command-Master
Add lemmi
3292af6
@Command-Master
Add leibniz_zpow
f276076
@Command-Master
merge rewrites
49f8b05
@Command-Master
Merge branch 'CommandMaster_leibdiv' into CommandMaster_DifferentialF…
b894eaa 
…ield
@Command-Master
Update
3b1c80f
@Command-Master
Add SharedConstants
85522ea
@Command-Master
Merge branch 'CommandMaster_diffring' into CommandMaster_Differential…
f4d70ec 
…Field
@Command-Master
Start
4e4e7b1
@Command-Master
Merge branch 'master' into CommandMaster_diffring
6ef60d5
@Command-Master
SharedConstants rfl
d64315a
@Command-Master
Update Mathlib.lean
f2b913f
@Command-Master Command-Master added the t-algebra Algebra (groups, rings, fields, etc) label Jul 18, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 18, 2024 •
edited
Loading

PR summary 65412c7c77

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.FieldTheory.Differential.Basic 926

Declarations diff

+ _root_.algebraMap.coe_logDeriv
+ logDeriv
+ logDeriv_algebraMap
+ logDeriv_div
+ logDeriv_eq_zero
+ logDeriv_mul
+ logDeriv_multisetProd
+ logDeriv_one
+ logDeriv_pow
+ logDeriv_prod
+ logDeriv_prod_of_eq_zero
+ logDeriv_zero

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.

@Command-Master Command-Master added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 18, 2024
@Command-Master Command-Master changed the title feat(Mathlib/FieldTheory): define differential fields and start with Liouville's theorem feat(Mathlib/FieldTheory): define differential fields Sep 6, 2024
@Command-Master Command-Master removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 6, 2024
YaelDillies
YaelDillies reviewed Sep 6, 2024
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 6, 2024
Command-Master and others added 2 commits September 7, 2024 05:58
@Command-Master @YaelDillies
Apply suggestions from code review
7b7eeb3 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@Command-Master
Update Basic.lean
94014da
@Command-Master Command-Master removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 7, 2024
YaelDillies
YaelDillies reviewed Sep 7, 2024
View reviewed changes
@Command-Master @YaelDillies
Apply suggestions from code review
e5c138e 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
YaelDillies approved these changes Sep 13, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 13, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 13, 2024
kim-em
kim-em reviewed Sep 14, 2024
View reviewed changes
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Sep 14, 2024

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 14, 2024

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

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Sep 14, 2024
@Command-Master Command-Master added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 14, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 14, 2024
@Command-Master
Copy link
Copy Markdown
Collaborator Author

Command-Master commented Sep 14, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Sep 14, 2024
@Command-Master
feat(Mathlib/FieldTheory): define differential fields (#14860)
0e1cd2e 
Define logarithmic derivatives and prove some properties.



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Daniel Weber <55664973+Command-Master@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 14, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Mathlib/FieldTheory): define differential fields [Merged by Bors] - feat(Mathlib/FieldTheory): define differential fields Sep 14, 2024
@mathlib-bors mathlib-bors bot closed this Sep 14, 2024
@mathlib-bors mathlib-bors bot deleted the CommandMaster_DifferentialField branch September 14, 2024 09:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@github-actions github-actions[bot] github-actions[bot] left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@Command-Master @YaelDillies @kim-em @leanprover-community-bot-assistant