Merge remote-tracking branch 'origin/master' into batteries-pr-testin… #190348
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
|
221 KB |
sha256:3a8794a645274d1007b04dffdd4a124b851584682e4154a474b12c9c0ae6d940
|
|