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

[Merged by Bors] - feat(category_theory/opposites): iso.unop #7400

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(category_theory/opposites): iso.unop #7400

wants to merge 5 commits into from

Commits on Apr 28, 2021

  1. feat(category_theory/opposites): iso.unop

    @jcommelin
    jcommelin authored Apr 28, 2021
    Configuration menu
    Copy the full SHA
    0978467 View commit details
    Browse the repository at this point in the history

Commits on May 4, 2021

  1. remove duplicate namespace

    @jcommelin
    jcommelin committed May 4, 2021
    Configuration menu
    Copy the full SHA
    1ef8168 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into jcommelin-patch-2

    @jcommelin
    jcommelin committed May 4, 2021
    Configuration menu
    Copy the full SHA
    8c2086d View commit details
    Browse the repository at this point in the history

  3. remove remove_op

    @jcommelin
    jcommelin committed May 4, 2021
    Configuration menu
    Copy the full SHA
    09f34b4 View commit details
    Browse the repository at this point in the history

  4. Update src/category_theory/opposites.lean 

    Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
    @jcommelin @b-mehta
    jcommelin and b-mehta authored May 4, 2021
    Configuration menu
    Copy the full SHA
    d8dae00 View commit details
    Browse the repository at this point in the history