Trigger CI for https://github.com/leanprover-community/batteries/pull… #187069
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#L790
@Finset.prod_image_of_pairwise_eq_one Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean#L793
@Finset.sum_image_of_pairwise_eq_zero Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/Group/Commute/Defs.lean#L151
@AddCommute.nsmul_nsmul simp can prove this:
|
|
Build:
Mathlib/Algebra/Group/Commute/Defs.lean#L151
@Commute.pow_pow simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/Basic.lean#L265
@inv_mul_cancel_right₀ simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/Basic.lean#L272
@inv_mul_cancel_left₀ simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/Defs.lean#L208
@mul_inv_cancel₀ simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/Defs.lean#L234
@mul_inv_cancel_right₀ simp can prove this:
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
import-graph
Expired
|
220 KB |
sha256:a1fbfe89d0f3bfcd28ba9c8fb3334fcbfdc46ecc501a67d1d18e74fe86613467
|
|