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, CategoryTheory): define light profinite sets #8676

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(Topology, CategoryTheory): define light profinite sets #8676

wants to merge 5 commits into from

Commits on Nov 28, 2023

  1. feat(Topology, CategoryTheory): define light profinite sets

    @dagurtomas
    dagurtomas committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    e3a5060 View commit details
    Browse the repository at this point in the history

  2. add line to mathlib

    @dagurtomas
    dagurtomas committed Nov 28, 2023
    Configuration menu
    Copy the full SHA
    7a65e42 View commit details
    Browse the repository at this point in the history

Commits on Nov 29, 2023

  1. Update Mathlib/Topology/Category/LightProfinite/Basic.lean 

    Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
    @dagurtomas @joelriou
    dagurtomas and joelriou committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    cb3884c View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Topology/Category/LightProfinite/Basic.lean 

    Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
    @dagurtomas @joelriou
    dagurtomas and joelriou committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    6b7d9de View commit details
    Browse the repository at this point in the history

  3. Joel's comment about universes

    @dagurtomas
    dagurtomas committed Nov 29, 2023
    Configuration menu
    Copy the full SHA
    c6c8622 View commit details
    Browse the repository at this point in the history