ERR_LIN: Line has more than 100 characters

ERR_LIN: Line has more than 100 characters

Process completed with exit code 123.

/home/lean/actions-runner/_work/mathlib/mathlib/src/combinatorics/additive/erdos_ginzburg_ziv.lean:266:8: invalid type ascription, term has type ∀ (a : {x // x ∈ s.to_enum_finset}) (ha : a ∈ s.to_enum_finset.attach) (a_1 : ?m_1[a, ha]) (f : mv_polynomial ?m_2[a, ha] ?m_3[a, ha]), (a_1 • f).total_degree ≤ f.total_degree but is expected to have type ∀ (b : {x // x ∈ s.to_enum_finset}), b ∈ s.to_enum_finset.attach → (b.val.fst • X b ^ (p - 1)).total_degree ≤ ?m_1 b state: 3 goals p : ℕ, _inst_1 : fact (nat.prime p), s : multiset (zmod p) ⊢ ∀ (b : {x // x ∈ s.to_enum_finset}), b ∈ s.to_enum_finset.attach → (b.val.fst • X b ^ (p - 1)).total_degree ≤ ?m_1 b p : ℕ, _inst_1 : fact (nat.prime p), s : multiset (zmod p) ⊢ {x // x ∈ s.to_enum_finset} → ℕ p : ℕ, _inst_1 : fact (nat.prime p), s : multiset (zmod p) ⊢ s.to_enum_finset.attach.sup (λ (i : {x // x ∈ s.to_enum_finset}), (X i ^ (p - 1)).total_degree) + s.to_enum_finset.attach.sup ?m_1 < 2 * p - 1

Process completed with exit code 1.

WRN_BRC: Probable misformatting of curly braces

WRN_BRC: Probable misformatting of curly braces

WRN_BRC: Probable misformatting of curly braces

WRN_BRC: Probable misformatting of curly braces

WRN_BRC: Probable misformatting of curly braces

WRN_BRC: Probable misformatting of curly braces

WRN_BRC: Probable misformatting of curly braces

The following actions uses node12 which is deprecated and will be forced to run on node16: actions/upload-artifact@v2. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/

/home/lean/actions-runner/_work/mathlib/mathlib/src/combinatorics/additive/erdos_ginzburg_ziv.lean:86:8: declaration 'list.take_min' uses sorry

/home/lean/actions-runner/_work/mathlib/mathlib/src/combinatorics/additive/erdos_ginzburg_ziv.lean:87:8: declaration 'list.drop_min' uses sorry

/home/lean/actions-runner/_work/mathlib/mathlib/src/combinatorics/additive/erdos_ginzburg_ziv.lean:88:8: declaration 'list.rtake_min' uses sorry

/home/lean/actions-runner/_work/mathlib/mathlib/src/combinatorics/additive/erdos_ginzburg_ziv.lean:89:8: declaration 'list.rdrop_min' uses sorry

/home/lean/actions-runner/_work/mathlib/mathlib/src/combinatorics/additive/erdos_ginzburg_ziv.lean:94:0: declaration 'list.drop_suffix_drop' uses sorry