Skip to content

Actions: leanprover-community/mathlib4

Actions

Cross off linked issues

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
sync_closed_tasks.yaml
3,552 workflow runs
3,552 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

feat(ModelTheory/Satisfiability): Fix universe on ModelsBoundedFormula, derive consequences for models in all universes Cross off linked issues #6586: Pull request #16674 closed by awainverse
September 10, 2024 15:36 14s modelsboundedformula_universe
modelsboundedformula_universe
September 10, 2024 15:36 14s
sync to master Cross off linked issues #6585: Pull request #16657 closed by yoh-tanimoto
September 10, 2024 09:42 10s master
master
September 10, 2024 09:42 10s
[Merged by Bors] - feat(CategoryTheory/Galois): topology of fundamental group Cross off linked issues #6584: Pull request #16441 closed by mathlib-bors bot
September 10, 2024 07:44 13s chrisflav-galois-topology
chrisflav-galois-topology
September 10, 2024 07:44 13s
[Merged by Bors] - feat(Topology/Group): density of submonoid/subgroup closure Cross off linked issues #6583: Pull request #16521 closed by mathlib-bors bot
September 9, 2024 16:01 11s YK-submonoid-closure
YK-submonoid-closure
September 9, 2024 16:01 11s
chore: update Mathlib dependencies 2024-09-09 Cross off linked issues #6582: Pull request #16623 closed by semorrison
September 9, 2024 10:16 13s update-dependencies-bot-use-only
update-dependencies-bot-use-only
September 9, 2024 10:16 13s
shorten proof of hc a bit Cross off linked issues #6581: Pull request #16613 closed by AlbertJ-314
September 9, 2024 00:25 Action required AlbertJ-314:PKU_PR_JacobsonNoether
AlbertJ-314:PKU_PR_JacobsonNoether
September 9, 2024 00:25 Action required
feat(Mathlib/Tactic/Widget/StringDiagram): support tensorHom Cross off linked issues #6580: Pull request #11080 closed by yuma-mizuno
September 8, 2024 15:52 13s ymizuno-string-tensorHom
ymizuno-string-tensorHom
September 8, 2024 15:52 13s
[Merged by Bors] - feat(KrullDimension): Order.height_eq_index_of_length_eq_height_last Cross off linked issues #6579: Pull request #16500 closed by mathlib-bors bot
September 7, 2024 09:42 13s joachim/height-refactor-part2
joachim/height-refactor-part2
September 7, 2024 09:42 13s
chore(SetTheory/Ordinal/Artihmetic): clean up pred API Cross off linked issues #6578: Pull request #15961 closed by vihdzp
September 7, 2024 00:54 11s vi.pred_ordinal_note
vi.pred_ordinal_note
September 7, 2024 00:54 11s
Merge master Cross off linked issues #6577: Pull request #16535 closed by D-Thomine
September 6, 2024 14:02 12s master
master
September 6, 2024 14:02 12s
Merge master Cross off linked issues #6576: Pull request #16534 closed by D-Thomine
September 6, 2024 14:01 10s master
master
September 6, 2024 14:01 10s
perf: right to left subgoal order Cross off linked issues #6575: Pull request #16495 closed by FR-vdash-bot
September 6, 2024 10:00 13s FR_tc_rtol
FR_tc_rtol
September 6, 2024 10:00 13s
[Merged by Bors] - chore(RingTheory/UniqueFactorizationDomain): make WfDvdMonoid α an abbreviation for IsWellFounded α DvdNotUnit Cross off linked issues #6574: Pull request #16145 closed by mathlib-bors bot
September 6, 2024 09:11 10s vi.wf_dvd
vi.wf_dvd
September 6, 2024 09:11 10s
duplicated definition of the pullback functor between over categories Cross off linked issues #6573: Issue #13998 closed by jcommelin
September 6, 2024 07:47 10s
September 6, 2024 07:47 10s
feat(Logic/Small/Defs): Small.{max u v, u} α Cross off linked issues #6572: Pull request #16516 closed by vihdzp
September 6, 2024 03:25 15s vi.small_fix
vi.small_fix
September 6, 2024 03:25 15s
[Merged by Bors] - fix(fun_prop): make fun_prop to see through abbrev Cross off linked issues #6571: Pull request #16512 closed by mathlib-bors bot
September 6, 2024 01:15 16s lecopivo/fun_prop_abbrev_fix
lecopivo/fun_prop_abbrev_fix
September 6, 2024 01:15 16s
[Merged by Bors] - feat: ENat.toNat_{zero,one} Cross off linked issues #6570: Pull request #16356 closed by mathlib-bors bot
September 5, 2024 20:53 10s toNat_zero_one
toNat_zero_one
September 5, 2024 20:53 10s
feat (Analysis/NormedSpace/Equidecomposability): Definition of Equidecomposability Cross off linked issues #6569: Pull request #15167 closed by Bergschaf
September 5, 2024 18:10 13s feat-(Analysis/NormedSpace/Equidecomposability)--Definition-of-Equidecomposability
feat-(Analysis/NormedSpace/Equidecomposability)--Definition-of-Equidecomposability
September 5, 2024 18:10 13s
Xyzw12345 patch 1 Cross off linked issues #6568: Pull request #16511 closed by xyzw12345
September 5, 2024 15:42 Action required jjdishere:xyzw12345-patch-1
jjdishere:xyzw12345-patch-1
September 5, 2024 15:42 Action required
[Merged by Bors] - feat(Algebra/Homology/Embedding): relation between K ⟶ L.extend e and K.restriction e ⟶ L Cross off linked issues #6567: Pull request #15768 closed by mathlib-bors bot
September 5, 2024 14:26 11s embedding-homequiv-1
embedding-homequiv-1
September 5, 2024 14:26 11s
[Merged by Bors] - feat(ModelTheory/Order): From order to structure and back Cross off linked issues #6566: Pull request #16373 closed by mathlib-bors bot
September 5, 2024 14:26 11s order_structure_instance
order_structure_instance
September 5, 2024 14:26 11s
chore: install gh in maintainer-merge workflows Cross off linked issues #6565: Pull request #16474 closed by jcommelin
September 5, 2024 09:21 11s jmc-maintainer-merge-gh
jmc-maintainer-merge-gh
September 5, 2024 09:21 11s
refactor (CatHasColimits): golf and format Cross off linked issues #6564: Pull request #16492 closed by pitmonticone
September 4, 2024 23:58 11s pitmonticone/CatHasColimits
pitmonticone/CatHasColimits
September 4, 2024 23:58 11s
Math olympiad Cross off linked issues #6563: Issue #16023 closed by joneugster
September 4, 2024 23:50 13s
September 4, 2024 23:50 13s
feat(Order/SuccPred/Inverse): "predecessor" from successor Cross off linked issues #6562: Pull request #16463 closed by vihdzp
September 4, 2024 18:03 10s vi.pred'
vi.pred'
September 4, 2024 18:03 10s