Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(FieldTheory/Galois): Fundamental theorem of infinite galois theory #16982

Open
wants to merge 165 commits into
base: master
Choose a base branch
from
Open

feat(FieldTheory/Galois): Fundamental theorem of infinite galois theory #16982

wants to merge 165 commits into from
+298 −0

Commits on Sep 20, 2024

  1. Create ClosedSubgroup.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    50972f4 View commit details
    Browse the repository at this point in the history

  2. Update ProfiniteGrp.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    f2c089d View commit details
    Browse the repository at this point in the history

  3. add continuous mul equiv

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    9027a87 View commit details
    Browse the repository at this point in the history

  4. add a theorem to ProfiniteGrp

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    9da7264 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    45bf888 View commit details
    Browse the repository at this point in the history

  6. move file Galois into folder Galois 

    For the incoming infinite case
    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    1c37547 View commit details
    Browse the repository at this point in the history

  7. add lemmas

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    fd67340 View commit details
    Browse the repository at this point in the history

  8. add finite Galois subextension

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    a3605e1 View commit details
    Browse the repository at this point in the history

  9. add more lemmas

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    8bf0b73 View commit details
    Browse the repository at this point in the history

  10. Update Mathlib.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    bee7c47 View commit details
    Browse the repository at this point in the history

  11. update import

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    ffd1d3d View commit details
    Browse the repository at this point in the history

  12. Merge branch 'closed-subgroup' into Fundamental-Theorem-of-Infinite-G… 

    …alois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    5ce8bcd View commit details
    Browse the repository at this point in the history

  13. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    602563d View commit details
    Browse the repository at this point in the history

  14. add Fundamental Theorem

    @Thmoas-Guan
    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    76d9e5c View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2024

  1. basic class instances

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    c4b9518 View commit details
    Browse the repository at this point in the history

  2. fix layout

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    079f9c5 View commit details
    Browse the repository at this point in the history

  3. coe instances

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    02a364a View commit details
    Browse the repository at this point in the history

  4. bijective lemmas

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    542d202 View commit details
    Browse the repository at this point in the history

  5. refl lemmas

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    ef9411e View commit details
    Browse the repository at this point in the history

  6. fix simpNF

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    c82bbcf View commit details
    Browse the repository at this point in the history

  7. fix simpNF

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    d77dc44 View commit details
    Browse the repository at this point in the history

  8. Update ContinuousMonoidHom.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    6f7e223 View commit details
    Browse the repository at this point in the history

  9. symm lemmas

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    b8c2c87 View commit details
    Browse the repository at this point in the history

  10. trans lemmas

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    0833559 View commit details
    Browse the repository at this point in the history

  11. refine notation

    @Thmoas-Guan
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    ccdb4d3 View commit details
    Browse the repository at this point in the history

Commits on Sep 22, 2024

  1. Update ClosedSubgroup.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    ceeefd2 View commit details
    Browse the repository at this point in the history

  2. Update ClosedSubgroup.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    18aac9a View commit details
    Browse the repository at this point in the history

  3. Update ClosedSubgroup.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    ca14e96 View commit details
    Browse the repository at this point in the history

  4. Update ClosedSubgroup.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    28d59db View commit details
    Browse the repository at this point in the history

  5. Merge branch 'closed-subgroup' into Fundamental-Theorem-of-Infinite-G… 

    …alois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    89b42d2 View commit details
    Browse the repository at this point in the history

  6. move lemma

    @Thmoas-Guan
    Thmoas-Guan committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    eaf6d41 View commit details
    Browse the repository at this point in the history

  7. move lemma

    @Thmoas-Guan
    Thmoas-Guan committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    3783f5c View commit details
    Browse the repository at this point in the history

  8. Merge branch 'closed-subgroup' into Fundamental-Theorem-of-Infinite-G… 

    …alois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    08df284 View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2024

  1. Update ContinuousMonoidHom.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    4b5dadb View commit details
    Browse the repository at this point in the history

  2. add coe to Homeomorph

    @Thmoas-Guan
    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    8d88664 View commit details
    Browse the repository at this point in the history

  3. add unique

    @Thmoas-Guan
    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    9cddc2a View commit details
    Browse the repository at this point in the history

  4. add map

    @Thmoas-Guan
    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    6cf5cd8 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'continuous-isomorphism' into Fundamental-Theorem-of-Inf… 

    …inite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    979bd09 View commit details
    Browse the repository at this point in the history

  6. Revert "Merge branch 'continuous-isomorphism' into Fundamental-Theore… 

    …m-of-Infinite-Galois-Theory"

This reverts commit 979bd09, reversing
changes made to 08df284.
    @Thmoas-Guan
    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    b14bbde View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2024

  1. Update Galois.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    72dd249 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'update-Galois' into lemmas-of-Galois-theory

    @Thmoas-Guan
    Thmoas-Guan committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    00288b9 View commit details
    Browse the repository at this point in the history

  3. Revert "Merge branch 'update-Galois' into lemmas-of-Galois-theory" 

    This reverts commit 00288b9, reversing
changes made to 8bf0b73.
    @Thmoas-Guan
    Thmoas-Guan committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    efabf3a View commit details
    Browse the repository at this point in the history

  4. Update Galois.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    180c3f9 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'update-Galois-for-merge' into lemmas-of-Galois-theory

    @Thmoas-Guan
    Thmoas-Guan committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    504d2c9 View commit details
    Browse the repository at this point in the history

  6. Revert "Merge branch 'update-Galois-for-merge' into lemmas-of-Galois-… 

    …theory"

This reverts commit 504d2c9, reversing
changes made to efabf3a.
    @Thmoas-Guan
    Thmoas-Guan committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    2241efa View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'upstream/master' into lemmas-of-Galois-… 

    …theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    ded38ae View commit details
    Browse the repository at this point in the history

  8. Merge branch 'Infinite-Galois-Theory-New-Base-ver' into finite-Galois… 

    …-subextensions
    @Thmoas-Guan
    Thmoas-Guan committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    149860e View commit details
    Browse the repository at this point in the history

  9. Merge branch 'Infinite-Galois-Theory-New-Base-ver' into Fundamental-T… 

    …heorem-of-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    5542978 View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2024

  1. Merge branch 'master' into finite-Galois-subextensions

    @Thmoas-Guan
    Thmoas-Guan authored Sep 28, 2024
    Configuration menu
    Copy the full SHA
    602e2de View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into lemmas-of-Galois-theory

    @Thmoas-Guan
    Thmoas-Guan authored Sep 28, 2024
    Configuration menu
    Copy the full SHA
    83a18b5 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 28, 2024
    Configuration menu
    Copy the full SHA
    458abe4 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 28, 2024
    Configuration menu
    Copy the full SHA
    170b300 View commit details
    Browse the repository at this point in the history

  5. fix Basic.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 28, 2024
    Configuration menu
    Copy the full SHA
    197ecbe View commit details
    Browse the repository at this point in the history

  6. fix docstring

    @Thmoas-Guan
    Thmoas-Guan committed Sep 28, 2024
    Configuration menu
    Copy the full SHA
    dacf676 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 28, 2024
    Configuration menu
    Copy the full SHA
    d91db4a View commit details
    Browse the repository at this point in the history

  8. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 28, 2024
    Configuration menu
    Copy the full SHA
    9c8bca5 View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2024

  1. Merge remote-tracking branch 'upstream/master' into Fundamental-Theor… 

    …em-of-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    2b6ea1d View commit details
    Browse the repository at this point in the history

  2. fix docstring

    @Thmoas-Guan
    Thmoas-Guan committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    46b037e View commit details
    Browse the repository at this point in the history

  3. Update InfiniteDimensional.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    a078700 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    3913ed8 View commit details
    Browse the repository at this point in the history

  5. update import

    @Thmoas-Guan
    Thmoas-Guan committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    d54c142 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'master' into Fundamental-Theorem-of-Infinite-Galois-Theory

    @Thmoas-Guan
    Thmoas-Guan authored Sep 29, 2024
    Configuration menu
    Copy the full SHA
    f74b3d6 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' into lemmas-of-Galois-theory

    @Thmoas-Guan
    Thmoas-Guan authored Sep 29, 2024
    Configuration menu
    Copy the full SHA
    e75cb4f View commit details
    Browse the repository at this point in the history

  8. Update InfiniteDimensional.lean

    @Thmoas-Guan
    Thmoas-Guan committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    9ad5bc3 View commit details
    Browse the repository at this point in the history

Commits on Sep 30, 2024

  1. use better definition

    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    09dac4f View commit details
    Browse the repository at this point in the history

  2. refine naming

    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    82e02bd View commit details
    Browse the repository at this point in the history

  3. Revert "add more lemmas" 

    This reverts commit 8bf0b73.
    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    d713a88 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    808ce63 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'upstream/Infinite-Galois-Theory-New-New… 

    …-Base-ver' into finite-Galois-subextensions
    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    22abb5c View commit details
    Browse the repository at this point in the history

  6. fix with new definition

    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    1b68667 View commit details
    Browse the repository at this point in the history

  7. fix layout

    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    ca14511 View commit details
    Browse the repository at this point in the history

  8. update docstring

    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    1d78e34 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    f43b9dc View commit details
    Browse the repository at this point in the history

  10. update naming in structure

    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    7855c4e View commit details
    Browse the repository at this point in the history

  11. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    c4ab3c6 View commit details
    Browse the repository at this point in the history

  12. update with new naming

    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    5525533 View commit details
    Browse the repository at this point in the history

  13. fix simpNF

    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    470e184 View commit details
    Browse the repository at this point in the history

  14. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    7b99b79 View commit details
    Browse the repository at this point in the history

  15. fix simpNF

    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    80e72b5 View commit details
    Browse the repository at this point in the history

  16. use better lemma

    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    3ad4b32 View commit details
    Browse the repository at this point in the history

  17. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    1fbbc58 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2024

  1. rearrange lemmas

    @Thmoas-Guan
    Thmoas-Guan committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    e06376b View commit details
    Browse the repository at this point in the history

  2. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    1a3ac94 View commit details
    Browse the repository at this point in the history

  3. add docstring

    @Thmoas-Guan
    Thmoas-Guan committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    2d394c7 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    c3591b0 View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2024

  1. refine layout

    @Thmoas-Guan
    Thmoas-Guan committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    90bcbb1 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    9e3aa14 View commit details
    Browse the repository at this point in the history

  3. rename added file

    @Thmoas-Guan
    Thmoas-Guan committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    4ee31ed View commit details
    Browse the repository at this point in the history

  4. Update Mathlib.lean

    @Thmoas-Guan
    Thmoas-Guan committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    b119405 View commit details
    Browse the repository at this point in the history

  5. refine docstring

    @Thmoas-Guan
    Thmoas-Guan committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    b1530de View commit details
    Browse the repository at this point in the history

  6. remove useless ext

    @Thmoas-Guan
    Thmoas-Guan committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    aa12c38 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    c10b4ac View commit details
    Browse the repository at this point in the history

  8. refine naming

    @Thmoas-Guan
    Thmoas-Guan committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    6ac7794 View commit details
    Browse the repository at this point in the history

  9. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 2, 2024
    Configuration menu
    Copy the full SHA
    1534f95 View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2024

  1. fix docstring

    @Thmoas-Guan
    Thmoas-Guan committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    c157d13 View commit details
    Browse the repository at this point in the history

  2. add GaloisInsertion and GaloisCoinsertion

    @Thmoas-Guan
    Thmoas-Guan committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    579c6c7 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    4af5abd View commit details
    Browse the repository at this point in the history

  4. fix docstring

    @Thmoas-Guan
    Thmoas-Guan committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    04916c2 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    62fe9a2 View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2024

  1. fix docstring

    @Thmoas-Guan
    Thmoas-Guan committed Oct 6, 2024
    Configuration menu
    Copy the full SHA
    5052b4e View commit details
    Browse the repository at this point in the history

  2. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 6, 2024
    Configuration menu
    Copy the full SHA
    72e29aa View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2024

  1. move thms with category

    @Thmoas-Guan
    Thmoas-Guan committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    57c4d69 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master' into finite-Galois-sub… 

    …extensions
    @Thmoas-Guan
    Thmoas-Guan committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    eb1fbeb View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'upstream/master' into lemmas-of-Galois-… 

    …theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    d2798b9 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'upstream/master' into finite-Galois-sub… 

    …extensions
    @Thmoas-Guan
    Thmoas-Guan committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    d43cd04 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'finite-Galois-subextensions' into Fundamental-Theorem-o… 

    …f-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    2ac5009 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    868960e View commit details
    Browse the repository at this point in the history

Commits on Oct 19, 2024

  1. Merge branch 'master' into Fundamental-Theorem-of-Infinite-Galois-Theory

    @Thmoas-Guan
    Thmoas-Guan authored Oct 19, 2024
    Configuration menu
    Copy the full SHA
    9328389 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into lemmas-of-Galois-theory

    @Thmoas-Guan
    Thmoas-Guan authored Oct 19, 2024
    Configuration menu
    Copy the full SHA
    5676ddd View commit details
    Browse the repository at this point in the history

  3. split Galois.Infinite 

    to split the basic constructions, profinite (stated categorically), and the fundamental theorem completely.
    @Thmoas-Guan
    Thmoas-Guan committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    fee1bcb View commit details
    Browse the repository at this point in the history

  4. Update Mathlib.lean

    @Thmoas-Guan
    Thmoas-Guan committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    368b8c5 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'Move-Infinite-Galois' into Fundamental-Theorem-of-Infin… 

    …ite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    fe0dfde View commit details
    Browse the repository at this point in the history

  6. Create Infinite.lean

    @Thmoas-Guan
    Thmoas-Guan committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    5dea0b7 View commit details
    Browse the repository at this point in the history

  7. Update Infinite.lean

    @Thmoas-Guan
    Thmoas-Guan committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    653517b View commit details
    Browse the repository at this point in the history

  8. Update Infinite.lean

    @Thmoas-Guan
    Thmoas-Guan committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    b4eba8f View commit details
    Browse the repository at this point in the history

  9. Update Mathlib.lean

    @Thmoas-Guan
    Thmoas-Guan committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    67d88dc View commit details
    Browse the repository at this point in the history

Commits on Oct 20, 2024

  1. Merge remote-tracking branch 'upstream/master' into Fundamental-Theor… 

    …em-of-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    0222f4b View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master' into Fundamental-Theor… 

    …em-of-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    615c82b View commit details
    Browse the repository at this point in the history

  3. Create Infinite.lean

    @Thmoas-Guan
    Thmoas-Guan committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    8ab45c8 View commit details
    Browse the repository at this point in the history

Commits on Oct 21, 2024

  1. Merge remote-tracking branch 'upstream/master' into Fundamental-Theor… 

    …em-of-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 21, 2024
    Configuration menu
    Copy the full SHA
    e54991b View commit details
    Browse the repository at this point in the history

Commits on Oct 23, 2024

  1. Merge remote-tracking branch 'upstream/Infinite-Galois-Theory-New-Bas… 

    …e-ver' into lemmas-of-Galois-theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    55ac2b8 View commit details
    Browse the repository at this point in the history

  2. refine proofs and statements

    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    42a3a43 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    74c61ce View commit details
    Browse the repository at this point in the history

  4. refine statement

    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    9961b62 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    d140926 View commit details
    Browse the repository at this point in the history

  6. remove duplicated lemma 

    and refine proofs at the same time
    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    c1a987e View commit details
    Browse the repository at this point in the history

  7. refine lemma

    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    ddeb93c View commit details
    Browse the repository at this point in the history

  8. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    fd27841 View commit details
    Browse the repository at this point in the history

  9. Update Infinite.lean

    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    fed37c2 View commit details
    Browse the repository at this point in the history

  10. add lemma

    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    0da8a4e View commit details
    Browse the repository at this point in the history

  11. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    19dca48 View commit details
    Browse the repository at this point in the history

  12. remove duplicated lemma

    @Thmoas-Guan
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    91cddd5 View commit details
    Browse the repository at this point in the history

Commits on Oct 24, 2024

  1. add API lemma

    @Thmoas-Guan
    Thmoas-Guan committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    5ce45d5 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    d97e8f7 View commit details
    Browse the repository at this point in the history

Commits on Oct 25, 2024

  1. refine proofs

    @Thmoas-Guan
    Thmoas-Guan committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    d5b9384 View commit details
    Browse the repository at this point in the history

  2. fix naming

    @Thmoas-Guan
    Thmoas-Guan committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    e4b45c6 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    c7d8ea9 View commit details
    Browse the repository at this point in the history

  4. use new lemma

    @Thmoas-Guan
    Thmoas-Guan committed Oct 25, 2024
    Configuration menu
    Copy the full SHA
    30e9c23 View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2024

  1. Merge remote-tracking branch 'upstream/master' into lemmas-of-Galois-… 

    …theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    8ac435e View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master' into Fundamental-Theor… 

    …em-of-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    44d82b1 View commit details
    Browse the repository at this point in the history

  3. fix synthInstance reaching maximal heartbeat

    @Thmoas-Guan
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    113eaa1 View commit details
    Browse the repository at this point in the history

  4. refine proofs 

    note: the exact number of heartbeats needed is 22133
    @Thmoas-Guan
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    3f4ba40 View commit details
    Browse the repository at this point in the history

  5. refine proof 

    using lemma already added better
    @Thmoas-Guan
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    6b15340 View commit details
    Browse the repository at this point in the history

  6. refine proofs

    @Thmoas-Guan
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    317555b View commit details
    Browse the repository at this point in the history

Commits on Oct 30, 2024

  1. fix syhth instance heartbeat completely 

    resolved by lowering the priority of `IntermediateField.instIsScalarTowerSubtypeMem` to 900, see proting note for reason
    @Thmoas-Guan
    Thmoas-Guan committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    05d75cc View commit details
    Browse the repository at this point in the history

  2. Revert "fix syhth instance heartbeat completely" 

    This reverts commit 05d75cc.
    @Thmoas-Guan
    Thmoas-Guan committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    471fc87 View commit details
    Browse the repository at this point in the history

Commits on Oct 31, 2024

  1. Merge remote-tracking branch 'upstream/master' into lemmas-of-Galois-… 

    …theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    dac416d View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master' into Fundamental-Theor… 

    …em-of-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    fef39b3 View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2024

  1. discard raise in heartbeat 

    the raise in heartbeat is no longer needed after the merge of #18436
    @Thmoas-Guan
    Thmoas-Guan committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    c6c7723 View commit details
    Browse the repository at this point in the history

  2. refine proofs

    @Thmoas-Guan
    Thmoas-Guan committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    071b878 View commit details
    Browse the repository at this point in the history

  3. refine proofs

    @Thmoas-Guan
    Thmoas-Guan committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    1e26a5a View commit details
    Browse the repository at this point in the history

  4. refine proofs

    @Thmoas-Guan
    Thmoas-Guan committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    dc1cd77 View commit details
    Browse the repository at this point in the history

Commits on Nov 6, 2024

  1. fix naming 

    1 fix namespace of restrictNormalHom_ker
2 fix naming of lift_algEquiv and add a basic API lemma for it
    @Thmoas-Guan
    Thmoas-Guan committed Nov 6, 2024
    Configuration menu
    Copy the full SHA
    458c8f2 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Nov 6, 2024
    Configuration menu
    Copy the full SHA
    677def5 View commit details
    Browse the repository at this point in the history

  3. fix proofs with new naming

    @Thmoas-Guan
    Thmoas-Guan committed Nov 6, 2024
    Configuration menu
    Copy the full SHA
    68b780b View commit details
    Browse the repository at this point in the history

Commits on Nov 13, 2024

  1. Merge remote-tracking branch 'upstream/master' into lemmas-of-Galois-… 

    …theory
    @Thmoas-Guan
    Thmoas-Guan committed Nov 13, 2024
    Configuration menu
    Copy the full SHA
    0ce709a View commit details
    Browse the repository at this point in the history

  2. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Nov 13, 2024
    Configuration menu
    Copy the full SHA
    e2dc873 View commit details
    Browse the repository at this point in the history

Commits on Nov 30, 2024

  1. refine layout 

    add a space

Co-authored-by: Thomas Browning <[email protected]>
    @Thmoas-Guan @tb65536
    Thmoas-Guan and tb65536 authored Nov 30, 2024
    Configuration menu
    Copy the full SHA
    48938a3 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master' into lemmas-of-Galois-… 

    …theory
    @Thmoas-Guan
    Thmoas-Guan committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    66601cb View commit details
    Browse the repository at this point in the history

  3. Merge branch 'lemmas-of-Galois-theory' of https://github.com/leanprov… 

    …er-community/mathlib4 into lemmas-of-Galois-theory
    @Thmoas-Guan
    Thmoas-Guan committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    57ea576 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'lemmas-of-Galois-theory' into Fundamental-Theorem-of-In… 

    …finite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Nov 30, 2024
    Configuration menu
    Copy the full SHA
    86630e9 View commit details
    Browse the repository at this point in the history

Commits on Dec 1, 2024

  1. Merge remote-tracking branch 'upstream/master' into Fundamental-Theor… 

    …em-of-Infinite-Galois-Theory
    @Thmoas-Guan
    Thmoas-Guan committed Dec 1, 2024
    Configuration menu
    Copy the full SHA
    bb7074e View commit details
    Browse the repository at this point in the history

Commits on Dec 2, 2024

  1. refine proofs

    @Thmoas-Guan
    Thmoas-Guan committed Dec 2, 2024
    Configuration menu
    Copy the full SHA
    c5003f0 View commit details
    Browse the repository at this point in the history

Commits on Dec 3, 2024

  1. refine proof 

    use intermediatefield.inclusion to reduce the proof of intermediatefield.finitedimensional_of_le
    @Thmoas-Guan
    Thmoas-Guan committed Dec 3, 2024
    Configuration menu
    Copy the full SHA
    1176a5f View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2024

  1. move lemma finiteDimensional_of_le

    @Thmoas-Guan
    Thmoas-Guan committed Dec 4, 2024
    Configuration menu
    Copy the full SHA
    bd0c8d6 View commit details
    Browse the repository at this point in the history