wip #186997
Annotations
10 errors
|
Build:
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean#L530
@Finsupp.prod_indicator_index_eq_prod_attach Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean#L530
@Finsupp.sum_indicator_index_eq_sum_attach Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean#L538
@Finsupp.sum_indicator_index Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/BigOperators/Finsupp/Basic.lean#L538
@Finsupp.prod_indicator_index 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:2bd92efe11e4bbe31b1a7b0b9c7432ad7a2045784d7c7cf64a0fbc61f455340c
|
|