Skip to content

Actions: leanprover-community/mathlib4

Actions

Run pre-commit and in-place update PR on push

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
pre-commit.yml
7,108 workflow runs
7,108 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

feat: elementary lemmas aiding computations with log⁺, Mark II Run pre-commit and in-place update PR on push #7008: Pull request #30729 opened by kebekus
29s kebekus:kebekus/posLog3
kebekus:kebekus/posLog3
29s
feat(CategoryTheory): strong generators Run pre-commit and in-place update PR on push #7007: Pull request #29519 synchronize by joelriou
24s joelriou:strong-generator
joelriou:strong-generator
24s
[Merged by Bors] - chore(CategoryTheory): add deprecated module for Localization.Monoidal Run pre-commit and in-place update PR on push #7006: Pull request #30728 opened by dagurtomas
30s dagurtomas:deprecate-monoidal-basic
dagurtomas:deprecate-monoidal-basic
30s
refactor(CategoryTheory/Generator): use ObjectProperty instead of Set Run pre-commit and in-place update PR on push #7005: Pull request #30269 synchronize by joelriou
49s joelriou:refactor-isseparating
joelriou:refactor-isseparating
49s
feat: grind annotations for Disjoint Run pre-commit and in-place update PR on push #7004: Pull request #28026 synchronize by chrisflav
27s kim-em:grind_disjoint
kim-em:grind_disjoint
27s
feat(CategoryTheory): closure under bounded colimits Run pre-commit and in-place update PR on push #7003: Pull request #30168 synchronize by joelriou
25s joelriou:object-property-colimits-closure-bounded
joelriou:object-property-colimits-closure-bounded
25s
feat(CategoryTheory/ObjectProperty): closure of a property under certain colimits Run pre-commit and in-place update PR on push #7002: Pull request #30160 synchronize by joelriou
27s joelriou:object-property-colimits-closure
joelriou:object-property-colimits-closure
27s
feat(CategoryTheory/ObjectProperty): closure of a property under certain limits Run pre-commit and in-place update PR on push #7001: Pull request #29854 synchronize by joelriou
28s joelriou:object-property-limits-closure
joelriou:object-property-limits-closure
28s
feat(Topology/KrullDimension): add subspace dimension inequality Run pre-commit and in-place update PR on push #7000: Pull request #29728 synchronize by ADA-Projects
27s ADA-Projects:krull-dim-extensions
ADA-Projects:krull-dim-extensions
27s
refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape Run pre-commit and in-place update PR on push #6999: Pull request #29881 synchronize by joelriou
37s joelriou:refactor-object-property-closed-under-limits-of-shape
joelriou:refactor-object-property-closed-under-limits-of-shape
37s
feat(CategoryTheory): the orthogonal-reflection construction Run pre-commit and in-place update PR on push #6998: Pull request #30492 synchronize by joelriou
29s joelriou:orthogonal-reflection-2
joelriou:orthogonal-reflection-2
29s
feat(CategoryTheory): LeftBousfield.W is stable under transfinite compositions Run pre-commit and in-place update PR on push #6997: Pull request #30509 synchronize by joelriou
31s joelriou:orthogonal-reflection-4
joelriou:orthogonal-reflection-4
31s
feat(CategoryTheory): local objects with respect to a MorphismProperty Run pre-commit and in-place update PR on push #6996: Pull request #30472 synchronize by joelriou
26s joelriou:orthogonal-reflection
joelriou:orthogonal-reflection
26s
feat(NumberField/Cyclotomic): splitting of the prime p in the p^k-th cyclotomic field Run pre-commit and in-place update PR on push #6995: Pull request #30682 synchronize by xroblot
24s xroblot:cyclo_primesplit_1
xroblot:cyclo_primesplit_1
24s
feat(NumberField/Cyclotomic): splitting of the prime p in the p^k-th cyclotomic field Run pre-commit and in-place update PR on push #6994: Pull request #30682 synchronize by xroblot
21s xroblot:cyclo_primesplit_1
xroblot:cyclo_primesplit_1
21s
Development branch (1) Run pre-commit and in-place update PR on push #6993: Pull request #30122 synchronize by pre-commit-ci-lite bot
23s xroblot:wip
xroblot:wip
23s
Development branch (1) Run pre-commit and in-place update PR on push #6992: Pull request #30122 synchronize by xroblot
25s xroblot:wip
xroblot:wip
25s
feat(CategoryTheory/Presentable): presentable objects in Type Run pre-commit and in-place update PR on push #6991: Pull request #30727 opened by joelriou
30s joelriou:presentable-type
joelriou:presentable-type
30s
feat(Homology) : Ext commute with flat base change Run pre-commit and in-place update PR on push #6990: Pull request #30532 synchronize by Thmoas-Guan
26s Thmoas-Guan:Ext-Base-Change
Thmoas-Guan:Ext-Base-Change
26s
feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection and equal distance Run pre-commit and in-place update PR on push #6989: Pull request #30477 synchronize by jsm28
21s jsm28:bisector_dist_oangle
jsm28:bisector_dist_oangle
21s
[Merged by Bors] - feat(Geometry/Euclidean/Angle/Oriented): oriented/unoriented equality and bisection lemmas Run pre-commit and in-place update PR on push #6988: Pull request #30476 synchronize by jsm28
24s jsm28:angle_eq_iff_oangle_eq_or_wbtw
jsm28:angle_eq_iff_oangle_eq_or_wbtw
24s
feat(Data/Setoid/Basic): add theorems about lifting a function to its kernel Run pre-commit and in-place update PR on push #6987: Pull request #28818 synchronize by SnirBroshi
24s SnirBroshi:feature/ker-lift
SnirBroshi:feature/ker-lift
24s
[Merged by Bors] - feat(Geometry/Euclidean/Angle/Oriented): oriented/unoriented equality and bisection lemmas Run pre-commit and in-place update PR on push #6986: Pull request #30476 synchronize by jsm28
32s jsm28:angle_eq_iff_oangle_eq_or_wbtw
jsm28:angle_eq_iff_oangle_eq_or_wbtw
32s
fix(Data/List/Sort): Deprecate and replace List.Sorted Run pre-commit and in-place update PR on push #6985: Pull request #30441 synchronize by linesthatinterlace
27s linesthatinterlace:sorted_deprecation
linesthatinterlace:sorted_deprecation
27s
feat(GroupTheory/FreeGroup/Orbit): The orbit of a point generated by parts of a free group can be "duplicated" Run pre-commit and in-place update PR on push #6984: Pull request #30130 synchronize by Bergschaf
27s Bergschaf:F_2_test
Bergschaf:F_2_test
27s