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

[Merged by Bors] - feat: topology on module over topological ring #16895

Closed
wants to merge 32 commits into from
Closed

[Merged by Bors] - feat: topology on module over topological ring #16895

wants to merge 32 commits into from

Commits on Sep 17, 2024

  1. feat: topology on module over topological ring

    @kbuzzard
    kbuzzard committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    136e363 View commit details
    Browse the repository at this point in the history

  2. copyright header

    @kbuzzard
    kbuzzard committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    135b78c View commit details
    Browse the repository at this point in the history

  3. add coinduced_sSup

    @kbuzzard
    kbuzzard committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    8362725 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Topology/Algebra/Module/Action.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @kbuzzard @eric-wieser
    kbuzzard and eric-wieser authored Sep 17, 2024
    Configuration menu
    Copy the full SHA
    52b51d7 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/Topology/Algebra/Module/Action.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @kbuzzard @eric-wieser
    kbuzzard and eric-wieser authored Sep 17, 2024
    Configuration menu
    Copy the full SHA
    e5420f7 View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/Topology/Algebra/Module/Action.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @kbuzzard @eric-wieser
    kbuzzard and eric-wieser authored Sep 17, 2024
    Configuration menu
    Copy the full SHA
    79f8017 View commit details
    Browse the repository at this point in the history

  7. reviewer comment

    @kbuzzard
    kbuzzard committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    aced064 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'kbuzzard-action-topology' of github.com:leanprover-comm… 

    …unity/mathlib4 into kbuzzard-action-topology
    @kbuzzard
    kbuzzard committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    3661c07 View commit details
    Browse the repository at this point in the history

  9. fix build

    @kbuzzard
    kbuzzard committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    a057c0a View commit details
    Browse the repository at this point in the history

  10. add file to Mathlib.lean

    @kbuzzard
    kbuzzard committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    6c96a51 View commit details
    Browse the repository at this point in the history

  11. change notation

    @kbuzzard
    kbuzzard committed Sep 17, 2024
    Configuration menu
    Copy the full SHA
    19a7b44 View commit details
    Browse the repository at this point in the history

  12. Update Mathlib/Topology/Algebra/Module/Action.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @kbuzzard @eric-wieser
    kbuzzard and eric-wieser authored Sep 17, 2024
    Configuration menu
    Copy the full SHA
    4b81f74 View commit details
    Browse the repository at this point in the history

Commits on Sep 19, 2024

  1. Update Mathlib/Topology/Algebra/Module/Action.lean

    @kbuzzard
    kbuzzard authored Sep 19, 2024
    Configuration menu
    Copy the full SHA
    1399873 View commit details
    Browse the repository at this point in the history

Commits on Oct 10, 2024

  1. Update Mathlib/Topology/Algebra/Module/Action.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @kbuzzard @eric-wieser
    kbuzzard and eric-wieser authored Oct 10, 2024
    Configuration menu
    Copy the full SHA
    fd4bea2 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Topology/Algebra/Module/Action.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @kbuzzard @eric-wieser
    kbuzzard and eric-wieser authored Oct 10, 2024
    Configuration menu
    Copy the full SHA
    5297c7c View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Topology/Algebra/Module/Action.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @kbuzzard @eric-wieser
    kbuzzard and eric-wieser authored Oct 10, 2024
    Configuration menu
    Copy the full SHA
    18fef7a View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Topology/Algebra/Module/Action.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @kbuzzard @eric-wieser
    kbuzzard and eric-wieser authored Oct 10, 2024
    Configuration menu
    Copy the full SHA
    b63fdf5 View commit details
    Browse the repository at this point in the history

  5. Update Mathlib/Topology/Order.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @kbuzzard @eric-wieser
    kbuzzard and eric-wieser authored Oct 10, 2024
    Configuration menu
    Copy the full SHA
    da75112 View commit details
    Browse the repository at this point in the history

  6. sorry the opposite proof

    @kbuzzard
    kbuzzard committed Oct 10, 2024
    Configuration menu
    Copy the full SHA
    1c5d852 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'kbuzzard-action-topology' of github.com:leanprover-comm… 

    …unity/mathlib4 into kbuzzard-action-topology
    @kbuzzard
    kbuzzard committed Oct 10, 2024
    Configuration menu
    Copy the full SHA
    0e062e5 View commit details
    Browse the repository at this point in the history

Commits on Oct 11, 2024

  1. fill the sorry

    @eric-wieser
    eric-wieser committed Oct 11, 2024
    Configuration menu
    Copy the full SHA
    0630ddc View commit details
    Browse the repository at this point in the history

  2. fix warnings

    @eric-wieser
    eric-wieser committed Oct 11, 2024
    Configuration menu
    Copy the full SHA
    753646e View commit details
    Browse the repository at this point in the history

Commits on Oct 14, 2024

  1. add mulopposite instance

    @kbuzzard
    kbuzzard committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    530332f View commit details
    Browse the repository at this point in the history

  2. rename action topology -> module topology

    @kbuzzard
    kbuzzard committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    fc364e5 View commit details
    Browse the repository at this point in the history

  3. move iso earlier

    @kbuzzard
    kbuzzard committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    8b75ee5 View commit details
    Browse the repository at this point in the history

Commits on Oct 15, 2024

  1. add docstring

    @kbuzzard
    kbuzzard committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    04bb014 View commit details
    Browse the repository at this point in the history

  2. rename Action.lean to ModuleTopology.lean

    @kbuzzard
    kbuzzard committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    f607fb7 View commit details
    Browse the repository at this point in the history

  3. rewrite/clarify/fix/extend comments.

    @kbuzzard
    kbuzzard committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    88d1ec6 View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Topology/Algebra/Module/Basic.lean 

    Co-authored-by: Eric Wieser <[email protected]>
    @kbuzzard @eric-wieser
    kbuzzard and eric-wieser authored Oct 15, 2024
    Configuration menu
    Copy the full SHA
    533b2be View commit details
    Browse the repository at this point in the history

Commits on Oct 19, 2024

  1. add of_continuous_id

    @kbuzzard
    kbuzzard committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    ad2d292 View commit details
    Browse the repository at this point in the history

  2. tiny golf

    @eric-wieser
    eric-wieser committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    f787ec4 View commit details
    Browse the repository at this point in the history

  3. one more

    @eric-wieser
    eric-wieser committed Oct 19, 2024
    Configuration menu
    Copy the full SHA
    ef2b10c View commit details
    Browse the repository at this point in the history