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

Jump to bottom

feat(Topology/Algebra/Field): ContinuousSMul for intermediate fields #18142

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

feat(Topology/Algebra/Field): ContinuousSMul for intermediate fields #18142

wants to merge 13 commits into from
+50 −0

Commits on Oct 23, 2024

  1. Update Field.lean

    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    e3d1d30 View commit details
    Browse the repository at this point in the history

  2. fix

    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    e2f3699 View commit details
    Browse the repository at this point in the history

  3. ContinuousSMul for subfield intermediate fields

    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    1e083bf View commit details
    Browse the repository at this point in the history

  4. Smul

    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    a7bfde3 View commit details
    Browse the repository at this point in the history

  5. Revert "ContinuousSMul for subfield intermediate fields" 

    This reverts commit 1e083bf.
    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    ff465bf View commit details
    Browse the repository at this point in the history

  6. Merge branch 'jiedong_jiang_continuous_smul_intermediate_field' of ht… 

    …tps://github.com/leanprover-community/mathlib4 into jiedong_jiang_continuous_smul_intermediate_field
    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    e3576a3 View commit details
    Browse the repository at this point in the history

  7. Revert "Merge branch 'jiedong_jiang_continuous_smul_intermediate_fiel… 

    …d' of https://github.com/leanprover-community/mathlib4 into jiedong_jiang_continuous_smul_intermediate_field"

This reverts commit e3576a3, reversing
changes made to ff465bf.
    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    8c75884 View commit details
    Browse the repository at this point in the history

  8. Reapply "ContinuousSMul for subfield intermediate fields" 

    This reverts commit ff465bf.
    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    fa5a1b2 View commit details
    Browse the repository at this point in the history

  9. remove covered import 

    move lemmas

typo

fix large import
    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    b5bd4dd View commit details
    Browse the repository at this point in the history

  10. Revert "remove covered import" 

    This reverts commit b5bd4dd.
    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    b5efa8a View commit details
    Browse the repository at this point in the history

  11. split file

    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    1ab79fb View commit details
    Browse the repository at this point in the history

  12. Update Mathlib.lean

    @jjdishere
    jjdishere committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    b0efef1 View commit details
    Browse the repository at this point in the history

Commits on Oct 28, 2024

  1. Merge branch 'master' into jiedong_jiang_continuous_smul_intermediate… 

    …_field'
    @jjdishere
    jjdishere committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    f47c38c View commit details
    Browse the repository at this point in the history