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.

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(Topology/Group/Profinite): Profinite group is limit of finite group #16992

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

Commits on Sep 20, 2024

  1. Update ProfiniteGrp.lean

    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    fd67dad View commit details
    Browse the repository at this point in the history
  2. Update ProfiniteGrp.lean

    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    0bfb53b View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    50972f4 View commit details
    Browse the repository at this point in the history
  4. Update ProfiniteGrp.lean

    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
  5. Update OpenSubgroup.lean

    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    93669a4 View commit details
    Browse the repository at this point in the history
  6. add continuous mul equiv

    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
  7. Configuration menu
    Copy the full SHA
    9da7264 View commit details
    Browse the repository at this point in the history
  8. Update Mathlib.lean

    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
  9. Configuration menu
    Copy the full SHA
    e971d2f View commit details
    Browse the repository at this point in the history
  10. Update OpenSubgroup.lean

    Thmoas-Guan committed Sep 20, 2024
    Configuration menu
    Copy the full SHA
    56427be View commit details
    Browse the repository at this point in the history
  11. Update OpenSubgroup.lean

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

Commits on Sep 21, 2024

  1. basic class instances

    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 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 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 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 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 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 committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    d77dc44 View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    6f7e223 View commit details
    Browse the repository at this point in the history
  9. symm lemmas

    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 committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    0833559 View commit details
    Browse the repository at this point in the history
  11. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Sep 21, 2024
    Configuration menu
    Copy the full SHA
    03da44f View commit details
    Browse the repository at this point in the history
  12. Configuration menu
    Copy the full SHA
    14f9a55 View commit details
    Browse the repository at this point in the history
  13. Configuration menu
    Copy the full SHA
    fe7f7af View commit details
    Browse the repository at this point in the history
  14. refine notation

    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
  15. Configuration menu
    Copy the full SHA
    71c477e View commit details
    Browse the repository at this point in the history

Commits on Sep 22, 2024

  1. Configuration menu
    Copy the full SHA
    ceeefd2 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    18aac9a View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    ca14e96 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    28d59db View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    81033f6 View commit details
    Browse the repository at this point in the history
  6. Update OpenSubgroup.lean

    Thmoas-Guan committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    22d99bc View commit details
    Browse the repository at this point in the history
  7. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Sep 22, 2024
    Configuration menu
    Copy the full SHA
    78b71f1 View commit details
    Browse the repository at this point in the history
  8. move lemma

    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
  9. Configuration menu
    Copy the full SHA
    30d6250 View commit details
    Browse the repository at this point in the history
  10. Configuration menu
    Copy the full SHA
    da57225 View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2024

  1. 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 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 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 committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    6cf5cd8 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    33abf7b View commit details
    Browse the repository at this point in the history
  6. Update ProfiniteGrp.lean

    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    bfe6f4c View commit details
    Browse the repository at this point in the history
  7. add preserve limit

    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    78944c0 View commit details
    Browse the repository at this point in the history
  8. add abbrev

    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    b7c18ce View commit details
    Browse the repository at this point in the history
  9. Configuration menu
    Copy the full SHA
    ba54b28 View commit details
    Browse the repository at this point in the history
  10. fix with new def

    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    58d7b26 View commit details
    Browse the repository at this point in the history
  11. Update ProfiniteGrp.lean

    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    51c5052 View commit details
    Browse the repository at this point in the history
  12. Configuration menu
    Copy the full SHA
    d54457d View commit details
    Browse the repository at this point in the history
  13. Update ProfiniteGrp.lean

    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    b323e47 View commit details
    Browse the repository at this point in the history
  14. rearrange files

    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    2be680c View commit details
    Browse the repository at this point in the history
  15. Update docstring

    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    a1af760 View commit details
    Browse the repository at this point in the history
  16. Configuration menu
    Copy the full SHA
    752a6ff View commit details
    Browse the repository at this point in the history
  17. rearrange files

    Thmoas-Guan committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    ea005a1 View commit details
    Browse the repository at this point in the history
  18. Update Mathlib.lean

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

Commits on Sep 24, 2024

  1. refine layout

    Thmoas-Guan committed Sep 24, 2024
    Configuration menu
    Copy the full SHA
    6cc5643 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    e2954a6 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2024

  1. refine docstring

    Thmoas-Guan committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    9ca1b8c View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    2de3b53 View commit details
    Browse the repository at this point in the history
  3. add todo

    dagurtomas committed Sep 27, 2024
    Configuration menu
    Copy the full SHA
    129006c View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2024

  1. refine proof

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

Commits on Sep 29, 2024

  1. Configuration menu
    Copy the full SHA
    160e25f View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    d237a57 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    7699ae8 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    d0fefb0 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    5e90673 View commit details
    Browse the repository at this point in the history
  6. fix naming

    Thmoas-Guan committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    6a1a275 View commit details
    Browse the repository at this point in the history
  7. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    e6c4be7 View commit details
    Browse the repository at this point in the history
  8. fix layout

    Thmoas-Guan committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    4368cd6 View commit details
    Browse the repository at this point in the history
  9. Configuration menu
    Copy the full SHA
    2698377 View commit details
    Browse the repository at this point in the history
  10. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Sep 29, 2024
    Configuration menu
    Copy the full SHA
    70b5805 View commit details
    Browse the repository at this point in the history
  11. Configuration menu
    Copy the full SHA
    fbdf631 View commit details
    Browse the repository at this point in the history
  12. Configuration menu
    Copy the full SHA
    950ea17 View commit details
    Browse the repository at this point in the history
  13. Configuration menu
    Copy the full SHA
    a3b5ea3 View commit details
    Browse the repository at this point in the history

Commits on Oct 1, 2024

  1. Configuration menu
    Copy the full SHA
    bd2212b View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    dc64612 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    91e47ca View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    1ff2e92 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2024

  1. Configuration menu
    Copy the full SHA
    3d0d5a7 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    a1dcf48 View commit details
    Browse the repository at this point in the history

Commits on Oct 14, 2024

  1. fix import problem

    by removing the two theorem using it
    Thmoas-Guan committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    4c93d2b View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    1539108 View commit details
    Browse the repository at this point in the history
  3. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    4738bb1 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    b5fce9b View commit details
    Browse the repository at this point in the history

Commits on Oct 17, 2024

  1. fix docstring

    Thmoas-Guan committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    f62e7fc View commit details
    Browse the repository at this point in the history
  2. fix docstring

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

Commits on Oct 18, 2024

  1. Update OpenSubgroup.lean

    Thmoas-Guan committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    9e563a0 View commit details
    Browse the repository at this point in the history
  2. Merge remote-tracking branch 'upstream/Infinite-Galois-Theory-New-Bas…

    …e-ver' into continuous-isomorphism
    Thmoas-Guan committed Oct 18, 2024
    Configuration menu
    Copy the full SHA
    b44ef59 View commit details
    Browse the repository at this point in the history

Commits on Oct 19, 2024

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

    …-Base-ver' into continuous-isomorphism
    Thmoas-Guan committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    a255eda View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    3f41bd1 View commit details
    Browse the repository at this point in the history
  3. Merge remote-tracking branch 'upstream/Infinite-Galois-Theory-New-New…

    …-Base-ver' into open-normal-subgroup-in-clopen-nhds
    Thmoas-Guan committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    15d439b View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    c090878 View commit details
    Browse the repository at this point in the history

Commits on Oct 21, 2024

  1. Configuration menu
    Copy the full SHA
    6f50182 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    2bbaa26 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    8738881 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    4e24e49 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 open-normal-subgroup-in-clopen-nhds
    Thmoas-Guan committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    b1f3d14 View commit details
    Browse the repository at this point in the history

Commits on Oct 26, 2024

  1. add instance

    and fix docstring
    Thmoas-Guan committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    0b49c65 View commit details
    Browse the repository at this point in the history
  2. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    9aadcb4 View commit details
    Browse the repository at this point in the history
  3. fix instance

    Thmoas-Guan committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    be1ac05 View commit details
    Browse the repository at this point in the history
  4. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    83ab8ed View commit details
    Browse the repository at this point in the history
  5. fix def

    Thmoas-Guan committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    7fd971c View commit details
    Browse the repository at this point in the history
  6. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Oct 26, 2024
    Configuration menu
    Copy the full SHA
    070f392 View commit details
    Browse the repository at this point in the history

Commits on Oct 27, 2024

  1. move lemma

    Thmoas-Guan committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    a1fa303 View commit details
    Browse the repository at this point in the history
  2. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    f46e204 View commit details
    Browse the repository at this point in the history

Commits on Oct 29, 2024

  1. refine proof with induction

    use `IsCompact.induction`_on to reconstruct proofs
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    510506d View commit details
    Browse the repository at this point in the history
  2. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    cde653a View commit details
    Browse the repository at this point in the history
  3. add missing docstring

    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    f0a504c View commit details
    Browse the repository at this point in the history
  4. Merge branch 'open-normal-subgroup-in-clopen-nhds' into profinite-gro…

    …up-is-limit-of-finite-group
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    5a70645 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    a9e4584 View commit details
    Browse the repository at this point in the history
  6. prove every clopen nhd of one contain an open subgroup

    also proved that every clopen nhd of one contain an open normal subgroup, but put in another file because of the need of more import.
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    a028fb6 View commit details
    Browse the repository at this point in the history
  7. Merge branch 'open-normal-subgroup-in-clopen-nhds-of-one' into profin…

    …ite-group-is-limit-of-finite-group
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    5c5a4d3 View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    82966d3 View commit details
    Browse the repository at this point in the history
  9. Configuration menu
    Copy the full SHA
    e772471 View commit details
    Browse the repository at this point in the history
  10. Configuration menu
    Copy the full SHA
    cfc7818 View commit details
    Browse the repository at this point in the history
  11. Merge remote-tracking branch 'upstream/master' into open-normal-subgr…

    …oup-in-clopen-nhds-of-one
    Thmoas-Guan committed Oct 29, 2024
    Configuration menu
    Copy the full SHA
    77353bc View commit details
    Browse the repository at this point in the history

Commits on Oct 30, 2024

  1. Configuration menu
    Copy the full SHA
    c3e6b8f View commit details
    Browse the repository at this point in the history
  2. Merge branch 'open-normal-subgroup-in-clopen-nhds-of-one' into profin…

    …ite-group-is-limit-of-finite-group
    Thmoas-Guan committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    6cbb225 View commit details
    Browse the repository at this point in the history
  3. fix proofs with new definition

    the change from definition (not canonical) and property into lemma describing existence
    Thmoas-Guan committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    0b6636b View commit details
    Browse the repository at this point in the history
  4. fix layout

    Including the following:
    1 : fix naming (including naming of props in the proof)
    2 : update docstring
    3 : use dot notation as possible
    Thmoas-Guan committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    ac49c16 View commit details
    Browse the repository at this point in the history
  5. update docstring

    Thmoas-Guan committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    7bc46ad View commit details
    Browse the repository at this point in the history
  6. remove terminal simp only

    Thmoas-Guan committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    95e4a73 View commit details
    Browse the repository at this point in the history
  7. update docstring

    also fix naming for the change from def to lemma
    Thmoas-Guan committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    e882944 View commit details
    Browse the repository at this point in the history
  8. Merge branch 'open-normal-subgroup-in-clopen-nhds-of-one' into profin…

    …ite-group-is-limit-of-finite-group
    Thmoas-Guan committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    0b4fd00 View commit details
    Browse the repository at this point in the history
  9. fix proof with new lemma

    Thmoas-Guan committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    3623826 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 profinite-group-i…

    …s-limit-of-finite-group
    Thmoas-Guan committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    ea429f1 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    45d9435 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    f4ce0ca View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    3207622 View commit details
    Browse the repository at this point in the history