This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
bump #121019
Annotations
3 errors and 7 warnings
src/combinatorics/additive/erdos_ginzburg_ziv.lean#L137
ERR_LIN: Line has more than 100 characters
|
src/combinatorics/additive/erdos_ginzburg_ziv.lean#L317
ERR_LIN: Line has more than 100 characters
|
|
src/combinatorics/additive/erdos_ginzburg_ziv.lean#L139
WRN_BRC: Probable misformatting of curly braces
|
src/combinatorics/additive/erdos_ginzburg_ziv.lean#L340
WRN_BRC: Probable misformatting of curly braces
|
src/combinatorics/additive/erdos_ginzburg_ziv.lean#L343
WRN_BRC: Probable misformatting of curly braces
|
src/combinatorics/additive/erdos_ginzburg_ziv.lean#L352
WRN_BRC: Probable misformatting of curly braces
|
src/combinatorics/additive/erdos_ginzburg_ziv.lean#L354
WRN_BRC: Probable misformatting of curly braces
|
src/combinatorics/additive/erdos_ginzburg_ziv.lean#L360
WRN_BRC: Probable misformatting of curly braces
|
src/combinatorics/additive/erdos_ginzburg_ziv.lean#L362
WRN_BRC: Probable misformatting of curly braces
|
The logs for this run have expired and are no longer available.
Loading