[Merged by Bors] - refactor(FieldTheory/KrullTopology): clean up `KrullTopology.lean` by mbkybky · Pull Request #22971 · leanprover-community/mathlib4

mbkybky · 2025-03-16T07:01:15Z

Clean up KrullTopology.lean by moving some lemmas to their appropriate locations in earlier files.

Also move some lemmas from IntermediateField/Adjoin/Defs.lean to IntermediateField/Basic.lean since they are used in the proofs of new theorems in IntermediateField/Algebraic.lean.

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

This reverts commit 8811edb.

This reverts commit 8e41976.

github-actions · 2025-03-16T07:02:13Z

PR summary d93beded55

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ _root_.im_finiteDimensional
+ finiteDimensional_map
+ fixedField_antitone
+ fixedField_bot
+ fixedField_le
+ fixedField_top
+ fixingSubgroup.antimono
+ fixingSubgroup_antitone
+ fixingSubgroup_bot
+ fixingSubgroup_le
+ fixingSubgroup_top
+ map_id
+ mem_bot_iff_fixed
+ mem_fixingSubgroup_iff
+ mem_range_algebraMap_iff_fixed
- IntermediateField.fixingSubgroup.antimono
- IntermediateField.fixingSubgroup_bot
- IntermediateField.fixingSubgroup_top
- IntermediateField.map_id
- IntermediateField.mem_fixingSubgroup_iff
- im_finiteDimensional

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).

tb65536 · 2025-03-16T16:00:47Z

Note that this PR overlaps with #22759

yhtq · 2025-03-16T17:14:39Z

I would suggest moving your upstream to my branch. Auto-merge can solve most of the conflicts I think.

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

Mathlib/FieldTheory/IntermediateField/Algebraic.lean

Mathlib/FieldTheory/Galois/Basic.lean

Mathlib/FieldTheory/KrullTopology.lean

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

Mathlib/FieldTheory/Galois/Basic.lean

github-actions · 2025-05-01T20:31:39Z

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

riccardobrasca · 2025-05-02T01:34:03Z

Thanks!

bors d+

mathlib-bors · 2025-05-02T01:34:06Z

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

mbkybky · 2025-05-02T03:05:02Z

bors r+

…22971) Clean up `KrullTopology.lean` by moving some lemmas to their appropriate locations in earlier files. Also move some lemmas from `IntermediateField/Adjoin/Defs.lean` to `IntermediateField/Basic.lean` since they are used in the proofs of new theorems in `IntermediateField/Algebraic.lean`. Co-authored-by: Yongle Hu <140475041+mbkybky@users.noreply.github.com> Co-authored-by: Yongle Hu <2065545849@qq.com> Co-authored-by: yhtq <1414672068@qq.com>

mathlib-bors · 2025-05-02T03:15:15Z

Pull request successfully merged into master.

Build succeeded:

…22971) Clean up `KrullTopology.lean` by moving some lemmas to their appropriate locations in earlier files. Also move some lemmas from `IntermediateField/Adjoin/Defs.lean` to `IntermediateField/Basic.lean` since they are used in the proofs of new theorems in `IntermediateField/Algebraic.lean`. Co-authored-by: Yongle Hu <140475041+mbkybky@users.noreply.github.com> Co-authored-by: Yongle Hu <2065545849@qq.com> Co-authored-by: yhtq <1414672068@qq.com>

yhtq and others added 20 commits March 10, 2025 16:57

refactor and add some easy lemmas about Galois theory

df1109d

fix style

c009390

fix

f2dd068

update

3f5a45f

update

eed61d8

update

e8490e6

fix

c866026

update

1106175

Update Mathlib/FieldTheory/Galois/Basic.lean

8811edb

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

Update Mathlib/FieldTheory/Galois/Basic.lean

0bd1fbb

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

Update Mathlib/FieldTheory/Galois/Basic.lean

ac27fd8

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

Revert "Update Mathlib/FieldTheory/Galois/Basic.lean"

8e41976

This reverts commit 8811edb.

Reapply "Update Mathlib/FieldTheory/Galois/Basic.lean"

2f3e6ac

This reverts commit 8e41976.

remove duplicated lemmma in KrullToplogy.lean

226f165

update

2dd3867

update

2bfcdd6

fix deprecated message

db24c97

change to alias

324a7e0

clean KrullTopology.lean

8727db4

Update SeparableDegree.lean

f7adb34

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Mar 16, 2025

mbkybky added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 16, 2025

mbkybky added 3 commits March 16, 2025 15:05

Update AbelRuffini.lean

03a708f

Update KrullTopology.lean

582e30e

more

e5526de

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 16, 2025

tb65536 mentioned this pull request Mar 16, 2025

feat: Refactor and add some easy lemmas about Galois theory #22759

Closed

mbkybky and others added 2 commits March 19, 2025 10:12

Update Mathlib/FieldTheory/IntermediateField/Basic.lean

516010b

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

use the existing variables line

2cd8d68

tb65536 reviewed Mar 19, 2025

View reviewed changes

Mathlib/FieldTheory/IntermediateField/Algebraic.lean Outdated Show resolved Hide resolved

mbkybky added 2 commits March 19, 2025 19:11

rename and generalize

bf7ccee

add periods

e6c4fc2

mbkybky requested a review from tb65536 April 30, 2025 02:18

tb65536 approved these changes Apr 30, 2025

View reviewed changes

Mathlib/FieldTheory/Galois/Basic.lean Outdated Show resolved Hide resolved

Mathlib/FieldTheory/KrullTopology.lean Outdated Show resolved Hide resolved

mbkybky added 3 commits April 30, 2025 14:56

Merge branch 'master' into mbkybky/clean_KrullTopology

420b06d

rename

a5414ab

fix

84f6e4e

tb65536 reviewed Apr 30, 2025

View reviewed changes

Mathlib/FieldTheory/KrullTopology.lean Outdated Show resolved Hide resolved

Update Mathlib/FieldTheory/KrullTopology.lean

395be35

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>

mbkybky requested a review from tb65536 May 1, 2025 06:31

tb65536 reviewed May 1, 2025

View reviewed changes

Mathlib/FieldTheory/Galois/Basic.lean Show resolved Hide resolved

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 1, 2025

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels May 2, 2025

add deprecated aliases

d93bede

mathlib-bors bot changed the title ~~refactor(FieldTheory/KrullTopology): clean up KrullTopology.lean~~ [Merged by Bors] - refactor(FieldTheory/KrullTopology): clean up KrullTopology.lean May 2, 2025

mathlib-bors bot closed this May 2, 2025

mathlib-bors bot deleted the mbkybky/clean_KrullTopology branch May 2, 2025 03:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(FieldTheory/KrullTopology): clean up `KrullTopology.lean`#22971

[Merged by Bors] - refactor(FieldTheory/KrullTopology): clean up `KrullTopology.lean`#22971
mbkybky wants to merge 34 commits intomasterfrom
mbkybky/clean_KrullTopology

mbkybky commented Mar 16, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Mar 16, 2025 •

edited

Loading

Declarations diff

Uh oh!

tb65536 commented Mar 16, 2025

Uh oh!

yhtq commented Mar 16, 2025 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented May 1, 2025

Uh oh!

riccardobrasca commented May 2, 2025

Uh oh!

mathlib-bors bot commented May 2, 2025

Uh oh!

mbkybky commented May 2, 2025

Uh oh!

mathlib-bors bot commented May 2, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

mbkybky commented Mar 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary d93beded55

Import changes for modified files

Declarations diff

Uh oh!

tb65536 commented Mar 16, 2025

Uh oh!

yhtq commented Mar 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented May 1, 2025

Uh oh!

riccardobrasca commented May 2, 2025

Uh oh!

mathlib-bors bot commented May 2, 2025

Uh oh!

mbkybky commented May 2, 2025

Uh oh!

mathlib-bors bot commented May 2, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

mbkybky commented Mar 16, 2025 •

edited

Loading

github-actions bot commented Mar 16, 2025 •

edited

Loading

yhtq commented Mar 16, 2025 •

edited

Loading