Skip to content

Actions: leanprover-community/mathlib4

Actions

Post PR summary comment

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
PR_summary.yml
26,979 workflow runs
26,979 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

feat: define ApproximateUnit and basic API Post PR summary comment #26822: Pull request #17787 synchronize by j-loreaux
October 28, 2024 04:27 45s j-loreaux/approximate-unit
j-loreaux/approximate-unit
October 28, 2024 04:27 45s
refactor(LinearAlgebra/BilinearForm/TensorProduct): Tensor products of bilinear maps Post PR summary comment #26821: Pull request #14988 synchronize by mans0954
October 28, 2024 04:27 57s mans0954/tensorDistrib
mans0954/tensorDistrib
October 28, 2024 04:27 57s
chore(Filter/Prod): drop Filter.prod, use SProd instead Post PR summary comment #26820: Pull request #18315 synchronize by urkud
October 28, 2024 04:20 48s YK-filter-prod-def
YK-filter-prod-def
October 28, 2024 04:20 48s
chore(SetTheory/Game/Domineering): narrow dsimp Post PR summary comment #26819: Pull request #18318 opened by LeoDog896
October 28, 2024 04:01 51s tristanfr.domineering-simp-only
tristanfr.domineering-simp-only
October 28, 2024 04:01 51s
[Merged by Bors] - chore: split Data.Set.Basic Post PR summary comment #26818: Pull request #18317 synchronize by kim-em
October 28, 2024 04:00 45s symmdiff
symmdiff
October 28, 2024 04:00 45s
[Merged by Bors] - chore: split Data.Set.Basic Post PR summary comment #26817: Pull request #18317 synchronize by kim-em
October 28, 2024 04:00 46s symmdiff
symmdiff
October 28, 2024 04:00 46s
[Merged by Bors] - chore: move contents of Data.Finite.Basic earlier Post PR summary comment #26816: Pull request #18316 synchronize by kim-em
October 28, 2024 03:35 45s rm_data_finite_basic
rm_data_finite_basic
October 28, 2024 03:35 45s
chore(Filter/Prod): drop Filter.prod, use SProd instead Post PR summary comment #26815: Pull request #18315 synchronize by urkud
October 28, 2024 03:34 51s YK-filter-prod-def
YK-filter-prod-def
October 28, 2024 03:34 51s
chore(Filter/Prod): drop Filter.prod, use SProd instead Post PR summary comment #26814: Pull request #18315 synchronize by urkud
October 28, 2024 03:25 50s YK-filter-prod-def
YK-filter-prod-def
October 28, 2024 03:25 50s
[Merged by Bors] - chore: move contents of Data.Finite.Basic earlier Post PR summary comment #26813: Pull request #18316 synchronize by kim-em
October 28, 2024 03:17 1m 2s rm_data_finite_basic
rm_data_finite_basic
October 28, 2024 03:17 1m 2s
[Merged by Bors] - chore: split Data.Set.Basic Post PR summary comment #26812: Pull request #18317 opened by kim-em
October 28, 2024 03:14 54s symmdiff
symmdiff
October 28, 2024 03:14 54s
[Merged by Bors] - chore: move contents of Data.Finite.Basic earlier Post PR summary comment #26811: Pull request #18316 synchronize by kim-em
October 28, 2024 03:13 46s rm_data_finite_basic
rm_data_finite_basic
October 28, 2024 03:13 46s
[Merged by Bors] - chore: move contents of Data.Finite.Basic earlier Post PR summary comment #26810: Pull request #18316 synchronize by kim-em
October 28, 2024 03:09 48s rm_data_finite_basic
rm_data_finite_basic
October 28, 2024 03:09 48s
chore(Filter/Prod): drop Filter.prod, use SProd instead Post PR summary comment #26809: Pull request #18315 opened by urkud
October 28, 2024 02:48 1m 2s YK-filter-prod-def
YK-filter-prod-def
October 28, 2024 02:48 1m 2s
[Merged by Bors] - chore: update Mathlib dependencies 2024-10-28 Post PR summary comment #26808: Pull request #18314 opened by mathlib4-update-dependencies-bot
October 28, 2024 02:31 44s update-dependencies-bot-use-only
update-dependencies-bot-use-only
October 28, 2024 02:31 44s
chore: reverse the import order of Multiset.Nodup and .Range Post PR summary comment #26807: Pull request #18313 opened by kim-em
October 28, 2024 02:23 53s flip_multiset_nodup_range
flip_multiset_nodup_range
October 28, 2024 02:23 53s
[Merged by Bors] - feat: lake exe unused Post PR summary comment #26806: Pull request #18156 synchronize by kim-em
October 28, 2024 02:07 49s unused_tool
unused_tool
October 28, 2024 02:07 49s
[Merged by Bors] - chore(Data/List): move the definition of finRange to Defs Post PR summary comment #26805: Pull request #18312 opened by urkud
October 28, 2024 02:02 58s YK-finrange-def
YK-finrange-def
October 28, 2024 02:02 58s
[Merged by Bors] - chore: split Mathlib.Topology.Algebra.UniformGroup Post PR summary comment #26804: Pull request #18311 opened by kim-em
October 28, 2024 01:55 47s split_uniformgroup
split_uniformgroup
October 28, 2024 01:55 47s
[Merged by Bors] - feat: ext lemmas for MultilinearMap Post PR summary comment #26803: Pull request #18308 synchronize by eric-wieser
October 28, 2024 00:33 52s eric-wieser/multilinear-ext
eric-wieser/multilinear-ext
October 28, 2024 00:33 52s
[Merged by Bors] - feat: lake exe unused Post PR summary comment #26802: Pull request #18156 synchronize by kim-em
October 28, 2024 00:30 55s unused_tool
unused_tool
October 28, 2024 00:30 55s
[Merged by Bors] - chore: update Mathlib dependencies 2024-10-28 Post PR summary comment #26801: Pull request #18310 opened by mathlib4-update-dependencies-bot
October 28, 2024 00:25 45s update-dependencies-bot-use-only
update-dependencies-bot-use-only
October 28, 2024 00:25 45s
[Merged by Bors] - feat: ext lemmas for MultilinearMap Post PR summary comment #26800: Pull request #18308 synchronize by eric-wieser
October 28, 2024 00:19 1m 18s eric-wieser/multilinear-ext
eric-wieser/multilinear-ext
October 28, 2024 00:19 1m 18s
[Merged by Bors] - feat: lake exe unused Post PR summary comment #26799: Pull request #18156 synchronize by kim-em
October 28, 2024 00:18 1m 8s unused_tool
unused_tool
October 28, 2024 00:18 1m 8s
[Merged by Bors] - feat: lake exe unused Post PR summary comment #26798: Pull request #18156 synchronize by kim-em
October 28, 2024 00:18 52s unused_tool
unused_tool
October 28, 2024 00:18 52s