Skip to content

feat(Topology/Algebra): Krasner's lemma#18444

Closed
jjdishere wants to merge 320 commits intomasterfrom
jiedong_jiang_is_krasner_1
Closed

feat(Topology/Algebra): Krasner's lemma#18444
jjdishere wants to merge 320 commits intomasterfrom
jiedong_jiang_is_krasner_1

Conversation

@jjdishere
Copy link
Collaborator

@jjdishere jjdishere commented Oct 30, 2024 •
edited
Loading

This PR defines the class IsKrasner K L and IsKrasnerNorm K L. And proves that given a complete nontrivially normed/rank-one-valued field, every algebraic normed/valued fields extension L/K satisfies IsKrasner K L. However, as the uniqueness extension of norm of such a field is not merged into Mathlib yet, we put this as a condition in the theorem.

Open in Gitpod

jjdishere and others added 30 commits September 13, 2024 17:08
@jjdishere
Update Mathlib.lean
1bed997
@jjdishere
Update AlgebraicClosure.lean
e1d0762
@jjdishere
remove condition
55d0693
@jjdishere
Update Basic.lean
3304b55
@jjdishere
Update Splits.lean
0de5911
@jjdishere
fix
1236b66
@jjdishere
fix
aa7ccba
@jjdishere
fix
c8a5f98
@jjdishere
fix
b1d42fd
@jjdishere
Update Field.lean
e90afad
@jjdishere
Merge branch 'jiedong_jiang_minpoly_lemma' into jiedong_jiang_minpoly…
b7b85a3 
…_split
@jjdishere
Update Field.lean
4dd7f6f
@alreadydone
Merge branch 'master' into IntermediateField_algClosure
4111c3d
@alreadydone
Merge branch 'master' into IntermediateField_algClosure
cb5b944
@alreadydone
empty
d8fa106
@alreadydone
fixes
89494b4
@alreadydone
more fixes
2d674d5
@alreadydone
more fixes
39bc129
@alreadydone
shake
87fd241
@jjdishere @Ruben-VandeVelde
Update Mathlib/Algebra/Associated/Basic.lean
82ee24d 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@jjdishere @Ruben-VandeVelde
Update Mathlib/Algebra/Associated/Basic.lean
5506205 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@alreadydone
Update Mathlib/FieldTheory/IntermediateField/Algebraic.lean
03a87ce
@alreadydone
Merge branch 'master' into IntermediateField_algClosure
d257812
@jjdishere @Ruben-VandeVelde
Update Mathlib/FieldTheory/Minpoly/Field.lean
11bec1f 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@jjdishere
remove change
b0a970c
@jjdishere
Merge branch 'jiedong_jiang_minpoly_split' of https://github.com/lean…
27151b0 
…prover-community/mathlib4 into jiedong_jiang_minpoly_split
@jjdishere
Update Field.lean
0fb14cd
@jjdishere
Merge branch 'master' into jiedong_jiang_minpoly_split
8dc6273
@jjdishere
Update Field.lean
e5b8d0b
@jjdishere
Merge branch 'master' into jiedong_jiang_irreducible'
1b41103
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 20, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 17, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 25, 2025
@mathlib4-dependent-issues-bot
Copy link
Collaborator

mathlib4-dependent-issues-bot commented Jan 25, 2025

This PR/issue depends on:

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 26, 2025
jjdishere
jjdishere commented Feb 26, 2025
View reviewed changes
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 31, 2025
@jjdishere jjdishere mentioned this pull request Jun 25, 2025
Closed
@jjdishere
Copy link
Collaborator Author

jjdishere commented Jun 25, 2025

This PR has been migrated to a fork-based workflow: #26390

@jjdishere jjdishere closed this Jun 25, 2025
@YaelDillies YaelDillies deleted the jiedong_jiang_is_krasner_1 branch August 17, 2025 11:42
mathlib-bors bot pushed a commit that referenced this pull request Mar 4, 2026
@jjdishere @pre-commit-ci-lite
feat(Analysis/Normed): Krasner's lemma (#26390)
cb40e0a 
This PR continues the work from #18444.

Original PR: #18444

Co-authored-by: Jiedong Jiang <emailboxofjjd@163.com>
Co-authored-by: jjdishere <emailboxofjjd@163.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
mathlib-bors bot pushed a commit that referenced this pull request Mar 4, 2026
@jjdishere @pre-commit-ci-lite
feat(Analysis/Normed): Krasner's lemma (#26390)
4a0fab5 
This PR continues the work from #18444.

Original PR: #18444

Co-authored-by: Jiedong Jiang <emailboxofjjd@163.com>
Co-authored-by: jjdishere <emailboxofjjd@163.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) migrated-to-fork t-algebra Algebra (groups, rings, fields, etc) t-analysis Analysis (normed *, calculus) t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-topology Topological spaces, uniform spaces, metric spaces, filters WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@jjdishere @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant @alreadydone @jcommelin