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

[Merged by Bors] - feat(data/finsupp/indicator, algebra/big_operators/finsupp): add some lemmas about finsupp.indicator #17413

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(data/finsupp/indicator, algebra/big_operators/finsupp): add some lemmas about finsupp.indicator #17413

wants to merge 5 commits into from

Commits on Nov 7, 2022

  1. feat(data/finsupp/indicator, algebra/big_operators/finsupp): add some… 

    … lemmas about `finsupp.indicator`
    @FR-vdash-bot
    FR-vdash-bot committed Nov 7, 2022
    Configuration menu
    Copy the full SHA
    bfb21d0 View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2023

  1. Merge branch 'master' into FR_indicator_lemmas

    @FR-vdash-bot
    FR-vdash-bot committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    4f5b1f9 View commit details
    Browse the repository at this point in the history

  2. fix

    @FR-vdash-bot
    FR-vdash-bot committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    064b190 View commit details
    Browse the repository at this point in the history

  3. fix

    @FR-vdash-bot
    FR-vdash-bot committed Feb 13, 2023
    Configuration menu
    Copy the full SHA
    62debd6 View commit details
    Browse the repository at this point in the history

Commits on Feb 14, 2023

  1. Update finsupp.lean

    @FR-vdash-bot
    FR-vdash-bot authored Feb 14, 2023
    Configuration menu
    Copy the full SHA
    283b790 View commit details
    Browse the repository at this point in the history