[Merged by Bors] - feat: port Data.List.BigOperators.Basic by jcommelin · Pull Request #1380 · leanprover-community/mathlib4

jcommelin · 2023-01-06T11:55:57Z

Initial file copy from mathport
Mathbin -> Mathlib; add import to Mathlib.lean

…perators.Basic

kim-em · 2023-01-07T02:31:00Z

The remaining errors are from to_additive not finding additivized versions of auxiliary lemmas:

./././Mathlib/Data/List/BigOperators/Basic.lean:139:2: error: application type mismatch
  Mathlib.Algebra.Group.Units._auxLemma.22
argument has type
  AddMonoid M
but function has type
  ∀ [inst : Monoid M], IsUnit 1 = True
./././Mathlib/Data/List/BigOperators/Basic.lean:147:2: error: (kernel) unknown constant 'List.sum_isAddUnit'
./././Mathlib/Data/List/BigOperators/Basic.lean:232:2: error: application type mismatch
  Mathlib.Algebra.Group.Commute._auxLemma.8
argument has type
  AddZeroClass M
but function has type
  ∀ [inst : MulOneClass M] (a : M), Commute a 1 = True
./././Mathlib/Data/List/BigOperators/Basic.lean:242:2: error: (kernel) unknown constant 'AddCommute.list_sum_right'
./././Mathlib/Data/List/BigOperators/Basic.lean:400:2: error: application type mismatch
  Mathlib.Algebra.Group.Basic._auxLemma.9
argument has type
  InvolutiveNeg G
but function has type
  ∀ [inst : InvolutiveInv G], Function.Involutive Inv.inv = True

@fpvandoorn, would you have a moment to look at this?

fpvandoorn · 2023-01-07T12:07:19Z

Everything that mentions _auxLemma is almost certainly #1149, fixed by #1314

Fix obvious build failures. WIP

…m/leanprover-community/mathlib4 into port/Data.List.BigOperators.Basic

…perators.Basic

hrmacbeth

bors d+

Mathlib/Data/List/BigOperators/Basic.lean

bors · 2023-01-09T20:12:38Z

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

jcommelin · 2023-01-10T07:35:09Z

bors r+

- 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>

bors · 2023-01-10T07:41:01Z

Pull request successfully merged into master.

Build succeeded:

Build
Lint style

Fix obvious build failures. WIP

- [x] depends on: #1380 Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: thirdsgames <thirdsgames2018@gmail.com> Co-authored-by: zeramorphic <zeramorphic@proton.me>

- [x] depends on: #1380 Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: thirdsgames <thirdsgames2018@gmail.com> Co-authored-by: zeramorphic <zeramorphic@proton.me> Co-authored-by: zeramorphic <50671761+zeramorphic@users.noreply.github.com>

- [x] depends on: #1380 Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: thirdsgames <thirdsgames2018@gmail.com> Co-authored-by: zeramorphic <zeramorphic@proton.me>

- [x] depends on #1380 Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

- 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>

- [x] depends on: #1380 Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: thirdsgames <thirdsgames2018@gmail.com> Co-authored-by: zeramorphic <zeramorphic@proton.me>

- [x] depends on: #1380 Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: thirdsgames <thirdsgames2018@gmail.com> Co-authored-by: zeramorphic <zeramorphic@proton.me> Co-authored-by: zeramorphic <50671761+zeramorphic@users.noreply.github.com>

- [x] depends on: #1380 Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: thirdsgames <thirdsgames2018@gmail.com> Co-authored-by: zeramorphic <zeramorphic@proton.me>

- [x] depends on #1380 Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

jcommelin and others added 7 commits January 6, 2023 11:54

Initial file copy from mathport

f665772

Mathbin -> Mathlib; add import to Mathlib.lean

1c42296

names and capitalization

259f06d

wip

3a7c809

wip

b38b399

wip

afce0a3

fixes

10c4d59

hrmacbeth added the mathlib-port This is a port of a theory file from mathlib. label Jan 6, 2023

zeramorphic mentioned this pull request Jan 7, 2023

[Merged by Bors] - feat: port Data.List.Join #1395

Closed

1 task

kim-em added 2 commits January 7, 2023 13:27

fixes

2ffd48d

Merge remote-tracking branch 'origin/master' into port/Data.List.BigO…

3af83dd

…perators.Basic

kim-em requested a review from fpvandoorn January 7, 2023 02:31

long lines

66a2231

zeramorphic mentioned this pull request Jan 7, 2023

[Merged by Bors] - feat: port Data.List.Count #1410

Closed

1 task

jcommelin added 2 commits January 7, 2023 16:47

Merge branch 'master' into port/Data.List.BigOperators.Basic

1af9231

linting

af08b52

zeramorphic mentioned this pull request Jan 7, 2023

[Merged by Bors] - feat: port Data.List.Zip #1416

Closed

1 task

casavaca added a commit that referenced this pull request Jan 8, 2023

Depend on #1380

1701be9

Fix obvious build failures. WIP

casavaca mentioned this pull request Jan 8, 2023

[Merged by Bors] - feat Port/data.list.big operators.lemmas #1423

Closed

1 task

ChrisHughes24 and others added 4 commits January 9, 2023 07:27

some fixes

035ca06

Merge branch 'port/Data.List.BigOperators.Basic' of https://github.co…

681a533

…m/leanprover-community/mathlib4 into port/Data.List.BigOperators.Basic

Merge remote-tracking branch 'origin/master' into port/Data.List.BigO…

4e01c93

…perators.Basic

minifixes

5ef7512

jcommelin added the awaiting-review label Jan 9, 2023

break long lines

6a132e3

hrmacbeth reviewed Jan 9, 2023

View reviewed changes

Mathlib/Data/List/BigOperators/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Data/List/BigOperators/Basic.lean Show resolved Hide resolved

Mathlib/Data/List/BigOperators/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Data/List/BigOperators/Basic.lean Show resolved Hide resolved

kim-em added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 9, 2023

kim-em removed the awaiting-review label Jan 9, 2023

process comments

d1ba89f

github-actions bot added the ready-to-merge This PR has been sent to bors. label Jan 10, 2023

bors bot changed the title ~~feat: port Data.List.BigOperators.Basic~~ [Merged by Bors] - feat: port Data.List.BigOperators.Basic Jan 10, 2023

bors bot closed this Jan 10, 2023

bors bot deleted the port/Data.List.BigOperators.Basic branch January 10, 2023 07:41

casavaca added a commit that referenced this pull request Jan 10, 2023

Depend on #1380

215e660

Fix obvious build failures. WIP

bors bot pushed a commit that referenced this pull request Jan 10, 2023

feat Port/data.list.big operators.lemmas (#1423)

f6f04c9

- [x] depends on #1380 Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

jcommelin pushed a commit that referenced this pull request Jan 23, 2023

feat Port/data.list.big operators.lemmas (#1423)

ac0e1ef

- [x] depends on #1380 Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: port Data.List.BigOperators.Basic#1380

[Merged by Bors] - feat: port Data.List.BigOperators.Basic#1380
jcommelin wants to merge 18 commits intomasterfrom
port/Data.List.BigOperators.Basic

jcommelin commented Jan 6, 2023

Uh oh!

kim-em commented Jan 7, 2023

Uh oh!

fpvandoorn commented Jan 7, 2023

Uh oh!

hrmacbeth left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

bors bot commented Jan 9, 2023

Uh oh!

jcommelin commented Jan 10, 2023

Uh oh!

bors bot commented Jan 10, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

Conversation

jcommelin commented Jan 6, 2023

Uh oh!

kim-em commented Jan 7, 2023

Uh oh!

fpvandoorn commented Jan 7, 2023

Uh oh!

hrmacbeth left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

bors bot commented Jan 9, 2023

Uh oh!

jcommelin commented Jan 10, 2023

Uh oh!

bors bot commented Jan 10, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants