Skip to content

Commit

Permalink
feat: port Data.List.BigOperators.Basic (#1380)
Browse files Browse the repository at this point in the history
- Initial file copy from mathport
- Mathbin -> Mathlib; add import to Mathlib.lean


Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
3 people committed Jan 10, 2023
1 parent 9a03164 commit 68d8ac5
Show file tree
Hide file tree
Showing 2 changed files with 675 additions and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Expand Up @@ -243,6 +243,7 @@ import Mathlib.Data.Int.Units
import Mathlib.Data.KVMap
import Mathlib.Data.LazyList
import Mathlib.Data.List.Basic
import Mathlib.Data.List.BigOperators.Basic
import Mathlib.Data.List.Card
import Mathlib.Data.List.Chain
import Mathlib.Data.List.Defs
Expand Down

0 comments on commit 68d8ac5

Please sign in to comment.