Trigger CI for https://github.com/leanprover-community/batteries/pull… #188488
Annotations
10 errors
|
Build:
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean#L538
@Finsupp.sum_indicator_index Left-hand side simplifies from
|
|
Build:
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean#L538
@Finsupp.prod_indicator_index Left-hand side simplifies from
|
|
Build:
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean#L51
@Finset.prod_insert_one simp can prove this:
|
|
Build:
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean#L53
@Finset.sum_insert_zero simp can prove this:
|
|
Build:
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean#L67
@Finset.sum_image Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean#L67
@Finset.prod_image Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/CubicDiscriminant.lean#L177
@Cubic.leadingCoeff_of_a_ne_zero' simp can prove this:
|
|
Build:
Mathlib/Algebra/CubicDiscriminant.lean#L185
@Cubic.leadingCoeff_of_b_ne_zero' simp can prove this:
|
|
Build:
Mathlib/Algebra/CubicDiscriminant.lean#L194
@Cubic.leadingCoeff_of_c_ne_zero' simp can prove this:
|
|
Build:
Mathlib/Algebra/CubicDiscriminant.lean#L258
@Cubic.degree_of_a_ne_zero' simp can prove this:
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
import-graph
Expired
|
220 KB |
sha256:56c14020e92750c3344a4d7e657f144ee6a1881cd2172120319d8d32f0ba3736
|
|