Skip to content

Actions: leanprover-community/mathlib4

Actions

Commit Verification

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
commit_verification.yml
24,191 workflow runs
24,191 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

refactor(RingTheory/Ideal/Heoght): minimize usages of Ideal.primeHeight and add lemma for minimalPrimes Commit Verification #24153: Pull request #37500 synchronize by Thmoas-Guan
40s Thmoas-Guan:minimalPrimes-API
Thmoas-Guan:minimalPrimes-API
40s
feat: semisimple eigenspace API and JC decomposition through ad Commit Verification #24152: Pull request #36697 synchronize by jano-wol
53s jano-wol:feature/semisimple-eigenspace-api
jano-wol:feature/semisimple-eigenspace-api
53s
chore: bump toolchain to v4.30.0-rc1 Commit Verification #24151: Pull request #37564 synchronize by Rob23oba
2m 22s leanprover-community:bump/v4.30.0
leanprover-community:bump/v4.30.0
2m 22s
feat: semisimple eigenspace API and JC decomposition through ad Commit Verification #24150: Pull request #36697 synchronize by jano-wol
43s jano-wol:feature/semisimple-eigenspace-api
jano-wol:feature/semisimple-eigenspace-api
43s
feat(RingTheory/Flat): finite flat algebra is trivial if rank is equal to 1 Commit Verification #24149: Pull request #36399 synchronize by chrisflav
37s chrisflav:flat-rank
chrisflav:flat-rank
37s
feat(RingTheory/Flat): finite flat algebra is trivial if rank is equal to 1 Commit Verification #24148: Pull request #36399 synchronize by chrisflav
41s chrisflav:flat-rank
chrisflav:flat-rank
41s
feat(RingTheory/Flat): finite flat algebra is trivial if rank is equal to 1 Commit Verification #24147: Pull request #36399 synchronize by chrisflav
11s chrisflav:flat-rank
chrisflav:flat-rank
11s
feat(RingTheory/Flat): finite flat algebra is trivial if rank is equal to 1 Commit Verification #24146: Pull request #36399 synchronize by chrisflav
11s chrisflav:flat-rank
chrisflav:flat-rank
11s
feat(RingTheory/Flat): finite flat algebra is trivial if rank is equal to 1 Commit Verification #24145: Pull request #36399 synchronize by chrisflav
35s chrisflav:flat-rank
chrisflav:flat-rank
35s
feat: set up API for ConvexSpace Commit Verification #24144: Pull request #37592 synchronize by erdOne
36s erdOne:erd1/APIConvexSpace
erdOne:erd1/APIConvexSpace
36s
feat(MeasureTheory/BorelSpace): add measurable_iSup_of_lowerSemicontinuous Commit Verification #24143: Pull request #37552 synchronize by pitmonticone
40s pitmonticone:carleson/measurable-biSup-continuousOn
pitmonticone:carleson/measurable-biSup-continuousOn
40s
feat(Combinatorics/SimpleGraph/Sum): add homomorphism, embedding and isomorphism of sums Commit Verification #24142: Pull request #37495 synchronize by IvanRenison
42s IvanRenison:Iso.sum
IvanRenison:Iso.sum
42s
feat: set up API for ConvexSpace Commit Verification #24141: Pull request #37592 opened by erdOne
39s erdOne:erd1/APIConvexSpace
erdOne:erd1/APIConvexSpace
39s
feat(Topology): implement delaborators for non-standard topology notation Commit Verification #24140: Pull request #31425 synchronize by robertmaxton42
40s robertmaxton42:delab_isFoo_of
robertmaxton42:delab_isFoo_of
40s
feat: semisimple eigenspace API and JC decomposition through ad Commit Verification #24139: Pull request #36697 synchronize by jano-wol
42s jano-wol:feature/semisimple-eigenspace-api
jano-wol:feature/semisimple-eigenspace-api
42s
feat: semisimple eigenspace API and JC decomposition through ad Commit Verification #24138: Pull request #36697 synchronize by jano-wol
44s jano-wol:feature/semisimple-eigenspace-api
jano-wol:feature/semisimple-eigenspace-api
44s
feat: semisimple eigenspace API and JC decomposition through ad Commit Verification #24137: Pull request #36697 synchronize by jano-wol
38s jano-wol:feature/semisimple-eigenspace-api
jano-wol:feature/semisimple-eigenspace-api
38s
feat: semisimple eigenspace API and JC decomposition through ad Commit Verification #24136: Pull request #36697 synchronize by jano-wol
40s jano-wol:feature/semisimple-eigenspace-api
jano-wol:feature/semisimple-eigenspace-api
40s
feat(RamificationInertia): add ramificationIdx_le_ramificationIdx and inertiaDeg_le_inertiaDeg Commit Verification #24135: Pull request #35405 synchronize by xroblot
37s xroblot:index_le_index
xroblot:index_le_index
37s
feat(MeasureTheory/BorelSpace): add measurable_iSup_of_lowerSemicontinuous Commit Verification #24134: Pull request #37552 synchronize by pitmonticone
39s pitmonticone:carleson/measurable-biSup-continuousOn
pitmonticone:carleson/measurable-biSup-continuousOn
39s
[Merged by Bors] - feat(MeasureTheory/Integral/Bochner): add exists_ne_zero_of_integral_ne_zero and exists_ne_zero_of_setIntegral_ne_zero Commit Verification #24133: Pull request #37568 synchronize by pitmonticone
41s pitmonticone:carleson/exists-ne-zero-integral
pitmonticone:carleson/exists-ne-zero-integral
41s
feat(AlgebraicTopology/SimplicialSet): more on nondegenerate simplices of the standard simplex Commit Verification #24132: Pull request #37332 synchronize by joelriou
37s joelriou:sset-stdsimplex-nondegenerateequiv
joelriou:sset-stdsimplex-nondegenerateequiv
37s
feat(RingTheory): regular local ring is domain Commit Verification #24131: Pull request #28683 synchronize by Thmoas-Guan
37s Thmoas-Guan:Regular-Local-Ring
Thmoas-Guan:Regular-Local-Ring
37s
feat: also use assumption to discharge gcongr side goals Commit Verification #24130: Pull request #37591 opened by grunweg
40s grunweg:gcongr-discharger
grunweg:gcongr-discharger
40s
feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation Commit Verification #24129: Pull request #26160 synchronize by yoh-tanimoto
39s oliver-butterley:variation-lemmas-1
oliver-butterley:variation-lemmas-1
39s