revert change in Mathlib.Data.ZMOD.Basic
#196006
Annotations
10 errors
|
Build:
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean#L73
@Finset.sum_image Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean#L73
@Finset.prod_image Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/Algebra/Group/Submonoid/Basic.lean#L305
@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#L305
@Submonoid.closure_sdiff_eq_closure Left-hand side does not simplify, when using the simp lemma on itself.
|
|
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#L235
@mul_inv_cancel_right₀ simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/Defs.lean#L241
@mul_inv_cancel_left₀ simp can prove this:
|
|
Build:
Mathlib/Algebra/GroupWithZero/NeZero.lean#L51
@inv_mul_cancel₀ simp can prove this:
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
import-graph
Expired
|
225 KB |
sha256:d7f29f6fed59192d65ed1102bd55056a7a828a1f4733af2f82765b6bc63405cf
|
|