wip #191337
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#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/Group/Commute/Hom.lean#L28
@SemiconjBy.of_map Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/Group/Commute/Hom.lean#L28
@AddSemiconjBy.of_map Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/Group/Commute/Hom.lean#L33
@Commute.of_map Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/Group/Commute/Hom.lean#L33
@AddCommute.of_map Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/Group/Submonoid/Basic.lean#L299
@AddSubmonoid.closure_sdiff_eq_closure Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/Group/Submonoid/Basic.lean#L299
@Submonoid.closure_sdiff_eq_closure Left-hand side does not simplify, when using the simp lemma on itself.
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
import-graph
Expired
|
222 KB |
sha256:e69b0740864ac336cd9da1b3ad9751590cdcb766b2f47513048d748c9468acc7
|
|