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: grind annotations for Disjoint Run pre-commit and in-place update PR on push #7033: Pull request #28026 synchronize by chrisflav
25s kim-em:grind_disjoint
kim-em:grind_disjoint
25s
chore: refactor using new by_cases! tactic Run pre-commit and in-place update PR on push #7032: Pull request #30073 synchronize by JovanGerb
21s JovanGerb:Jovan-by_cases!
JovanGerb:Jovan-by_cases!
21s
fix(AlgebraicTopology/SimplexCategory/GeneratorsRelations): ungrind IsAdmissible.singleton Run pre-commit and in-place update PR on push #7031: Pull request #30732 opened by robin-carlier
29s robin-carlier:fix_30586
robin-carlier:fix_30586
29s
feat: new by_cases! tactic Run pre-commit and in-place update PR on push #7030: Pull request #30730 synchronize by JovanGerb
23s JovanGerb:Jovan-by_cases-impl
JovanGerb:Jovan-by_cases-impl
23s
feat: define the Eisenstein Series E2 Run pre-commit and in-place update PR on push #7029: Pull request #26014 synchronize by CBirkbeck
23s CBirkbeck:CB_Eisenstein_E2
CBirkbeck:CB_Eisenstein_E2
23s
feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/NormalForms): Normal forms for P_δs Run pre-commit and in-place update PR on push #7028: Pull request #25737 synchronize by robin-carlier
22s robin-carlier:RC_SimplexCategoryGenRel6
robin-carlier:RC_SimplexCategoryGenRel6
22s
feat: new by_cases! tactic Run pre-commit and in-place update PR on push #7027: Pull request #30730 synchronize by JovanGerb
25s JovanGerb:Jovan-by_cases-impl
JovanGerb:Jovan-by_cases-impl
25s
feat(CategoryTheory/Presentable): transport via an equivalence Run pre-commit and in-place update PR on push #7026: Pull request #30731 opened by joelriou
25s joelriou:presentable-equivalence
joelriou:presentable-equivalence
25s
feat: define the Eisenstein Series E2 Run pre-commit and in-place update PR on push #7025: Pull request #26014 synchronize by CBirkbeck
23s CBirkbeck:CB_Eisenstein_E2
CBirkbeck:CB_Eisenstein_E2
23s
feat: new by_cases! tactic Run pre-commit and in-place update PR on push #7024: Pull request #30730 opened by JovanGerb
30s JovanGerb:Jovan-by_cases-impl
JovanGerb:Jovan-by_cases-impl
30s
feat(Geometry/Convex/Cone): add conical combinations and conical hull Run pre-commit and in-place update PR on push #7023: Pull request #27578 synchronize by bjornsolheim
20s bjornsolheim:bjornsolheim_conicalcombinations_conicalhull
bjornsolheim:bjornsolheim_conicalcombinations_conicalhull
20s
feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality for angles Run pre-commit and in-place update PR on push #7022: Pull request #26129 synchronize by LessnessRandomness
25s LessnessRandomness:triangle_theorem_for_angles
LessnessRandomness:triangle_theorem_for_angles
25s
chore: refactor using new by_cases! tactic Run pre-commit and in-place update PR on push #7021: Pull request #30073 synchronize by JovanGerb
31s JovanGerb:Jovan-by_cases!
JovanGerb:Jovan-by_cases!
31s
feat(CategoryTheory): localization of locally presentable categories Run pre-commit and in-place update PR on push #7020: Pull request #30554 synchronize by joelriou
30s joelriou:orthogonal-reflection-6
joelriou:orthogonal-reflection-6
30s
feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality for angles Run pre-commit and in-place update PR on push #7019: Pull request #26129 synchronize by LessnessRandomness
24s LessnessRandomness:triangle_theorem_for_angles
LessnessRandomness:triangle_theorem_for_angles
24s
feat(CategoryTheory): the universal property of localized monoidal categories Run pre-commit and in-place update PR on push #7018: Pull request #25799 synchronize by dagurtomas
24s dagurtomas:dagur/loc-mon-up
dagurtomas:dagur/loc-mon-up
24s
feat(CategoryTheory): orthogonal-reflection construction: existence of the left adjoint Run pre-commit and in-place update PR on push #7017: Pull request #30513 synchronize by joelriou
30s joelriou:orthogonal-reflection-5
joelriou:orthogonal-reflection-5
30s
feat(CategoryTheory): MorphismProperty.rightOrthogonal is closed under κ-filtered colimits Run pre-commit and in-place update PR on push #7016: Pull request #30507 synchronize by joelriou
28s joelriou:orthogonal-reflection-3
joelriou:orthogonal-reflection-3
28s
feat(CategoryTheory): presentable objects and adjunctions Run pre-commit and in-place update PR on push #7015: Pull request #30533 synchronize by joelriou
35s joelriou:presentable-adjunction
joelriou:presentable-adjunction
35s
feat(CategoryTheory): κ-presentable objects in a κ-accessible category is an essentially small category Run pre-commit and in-place update PR on push #7014: Pull request #30464 synchronize by joelriou
31s joelriou:essential-smallness-ispresentable
joelriou:essential-smallness-ispresentable
31s
feat(CategoryTheory): the universal property of localized monoidal categories Run pre-commit and in-place update PR on push #7013: Pull request #25799 synchronize by dagurtomas
34s dagurtomas:dagur/loc-mon-up
dagurtomas:dagur/loc-mon-up
34s
refactor(CategoryTheory/Presentable): cleaning up HasCardinalFilteredGenerator(s) Run pre-commit and in-place update PR on push #7012: Pull request #30459 synchronize by joelriou
31s joelriou:refactor-are-cardinal-filtered-generators
joelriou:refactor-are-cardinal-filtered-generators
31s
feat(CategoryTheory): dense functors Run pre-commit and in-place update PR on push #7011: Pull request #29565 synchronize by joelriou
30s joelriou:dense-functor
joelriou:dense-functor
30s
feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality for angles Run pre-commit and in-place update PR on push #7010: Pull request #26129 synchronize by LessnessRandomness
24s LessnessRandomness:triangle_theorem_for_angles
LessnessRandomness:triangle_theorem_for_angles
24s
feat(CategoryTheory): a property of objects is a strong generator if any object is a colimit of objects satisfying the property Run pre-commit and in-place update PR on push #7009: Pull request #29543 synchronize by joelriou
24s joelriou:strong-generator-of-colimit
joelriou:strong-generator-of-colimit
24s