Merge branch 'lean-pr-testing-8419' of github.com:leanprover-communit… #192846
nomeataAnnotations
10 errors
|
Build:
Mathlib/Data/ENNReal/Operations.lean#L295
@ENNReal.top_sub_coe simp can prove this:
|
|
Build:
Mathlib/Data/Finset/Sym.lean#L207
@Finset.sym_empty Left-hand side simplifies from
|
|
Build:
Mathlib/Data/Matrix/Basic.lean#L488
@LinearEquiv.entryLinearMap_comp_mapMatrix simp can prove this:
|
|
Build:
Mathlib/Data/Seq/Seq.lean#L410
@stream'.Seq.terminatedAt_nil Left-hand side does not simplify, when using the simp lemma on itself.
|
|
Build:
Mathlib/GroupTheory/QuotientGroup/Basic.lean#L84
@QuotientGroup.kerLift_mk' simp can prove this:
|
|
Build:
Mathlib/GroupTheory/QuotientGroup/Basic.lean#L84
@QuotientAddGroup.kerLift_mk' simp can prove this:
|
|
Build:
Mathlib/LinearAlgebra/Isomorphisms.lean#L154
@Submodule.quotientQuotientEquivQuotientAux_mk_mk simp can prove this:
|
|
Build:
Mathlib/RingTheory/Ideal/Quotient/Operations.lean#L566
@Ideal.quotientEquiv_symm_mk Left-hand side simplifies from
|
|
Build:
Mathlib/RingTheory/PowerSeries/Inverse.lean#L155
@PowerSeries.invOfUnit_eq simp can prove this:
|
|
Build
The process '/usr/bin/env' failed with exit code 1
|
Artifacts
Produced during runtime
| Name | Size | Digest | |
|---|---|---|---|
|
import-graph
Expired
|
223 KB |
sha256:8998067ba29644350cd3aa977e5cbaa5763474b6c2396fcca692c862a4215248
|
|