Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(topology/algebra): Inf and inducing preserve compatibility with algebraic structure #11720

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat(topology/algebra): Inf and inducing preserve compatibility with algebraic structure #11720

wants to merge 10 commits into from

Commits on Jan 23, 2022

  1. Begin

    @ADedecker
    ADedecker committed Jan 23, 2022
    Configuration menu
    Copy the full SHA
    a5cda78 View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2022

  1. Merge remote-tracking branch 'origin/master' into AD_top_lattice_algebra

    @ADedecker
    ADedecker committed Jan 27, 2022
    Configuration menu
    Copy the full SHA
    fb3abc6 View commit details
    Browse the repository at this point in the history

Commits on Jan 29, 2022

  1. Finish

    @ADedecker
    ADedecker committed Jan 29, 2022
    Configuration menu
    Copy the full SHA
    ec3fafb View commit details
    Browse the repository at this point in the history

Commits on Jan 30, 2022

  1. Temporary fix ?

    @ADedecker
    ADedecker committed Jan 30, 2022
    Configuration menu
    Copy the full SHA
    02cfd28 View commit details
    Browse the repository at this point in the history

  2. Uninstancify

    @ADedecker
    ADedecker committed Jan 30, 2022
    Configuration menu
    Copy the full SHA
    263dace View commit details
    Browse the repository at this point in the history

  3. Part 2

    @ADedecker
    ADedecker committed Jan 30, 2022
    Configuration menu
    Copy the full SHA
    0859497 View commit details
    Browse the repository at this point in the history

Commits on Jan 31, 2022

  1. Update basic.lean

    @ADedecker
    ADedecker committed Jan 31, 2022
    Configuration menu
    Copy the full SHA
    dc5112e View commit details
    Browse the repository at this point in the history

  2. ++

    @ADedecker
    ADedecker committed Jan 31, 2022
    Configuration menu
    Copy the full SHA
    470b187 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'AD_top_lattice_algebra' of github.com:leanprover-commun… 

    …ity/mathlib into AD_top_lattice_algebra
    @ADedecker
    ADedecker committed Jan 31, 2022
    Configuration menu
    Copy the full SHA
    87834b9 View commit details
    Browse the repository at this point in the history

Commits on Feb 3, 2022

  1. Remove priorities

    @ADedecker
    ADedecker committed Feb 3, 2022
    Configuration menu
    Copy the full SHA
    3e535c0 View commit details
    Browse the repository at this point in the history