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

[Merged by Bors] - chore(topology/algebra/infinite_sum): small todo #7994

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore(topology/algebra/infinite_sum): small todo #7994

wants to merge 3 commits into from

Commits on Jun 19, 2021

  1. typeclass todo

    @hrmacbeth
    hrmacbeth committed Jun 19, 2021
    Configuration menu
    Copy the full SHA
    4dc4ada View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review 

    Co-authored-by: damiano <adomani@gmail.com>
    @hrmacbeth @adomani
    hrmacbeth and adomani authored Jun 19, 2021
    Configuration menu
    Copy the full SHA
    62f5381 View commit details
    Browse the repository at this point in the history

Commits on Jun 20, 2021

  1. Update src/topology/algebra/infinite_sum.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @hrmacbeth @eric-wieser
    hrmacbeth and eric-wieser authored Jun 20, 2021
    Configuration menu
    Copy the full SHA
    bfa1a80 View commit details
    Browse the repository at this point in the history