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(Geometry/Euclidean/Projection): projection onto sup Run pre-commit and in-place update PR on push #7083: Pull request #30703 synchronize by jsm28
36s jsm28:orthogonalProjection_sup_of_orthogonalProjection_eq
jsm28:orthogonalProjection_sup_of_orthogonalProjection_eq
36s
chore: remove redundant fields from instances Run pre-commit and in-place update PR on push #7082: Pull request #30734 synchronize by JovanGerb
29s JovanGerb:Jovan-remove_instance_fields
JovanGerb:Jovan-remove_instance_fields
29s
chore(MeasureTheory/Function/SimpleFunc): deprecate SimpleFunc.coe_le Run pre-commit and in-place update PR on push #7081: Pull request #30737 opened by JovanGerb
33s JovanGerb:Jovan-SimpleFunc.coe_le
JovanGerb:Jovan-SimpleFunc.coe_le
33s
feat(Algebra/Polynomial/Factors): Introduce predicate and basic API Run pre-commit and in-place update PR on push #7080: Pull request #30212 synchronize by tb65536
33s tb65536:tb_sp
tb65536:tb_sp
33s
feat(Algebra/Polynomial/Factors): Introduce predicate and basic API Run pre-commit and in-place update PR on push #7079: Pull request #30212 synchronize by tb65536
35s tb65536:tb_sp
tb65536:tb_sp
35s
feat(gcongr): support @[gcongr] for Monotone and friends Run pre-commit and in-place update PR on push #7078: Pull request #28339 synchronize by JovanGerb
35s JovanGerb:Jovan-gcongr-Monotone
JovanGerb:Jovan-gcongr-Monotone
35s
feat(Algebra): generalize Picard group to Semiring Run pre-commit and in-place update PR on push #7077: Pull request #30657 synchronize by alreadydone
33s alreadydone:PicSemiring+
alreadydone:PicSemiring+
33s
feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup Run pre-commit and in-place update PR on push #7076: Pull request #30736 opened by alreadydone
42s alreadydone:Pic=ClassGroup
alreadydone:Pic=ClassGroup
42s
(WIP) Galois group of x^n - x - 1 Run pre-commit and in-place update PR on push #7075: Pull request #27053 synchronize by tb65536
32s tb65536:tb_selmer2
tb65536:tb_selmer2
32s
feat(Algebra): generalize Picard group to Semiring Run pre-commit and in-place update PR on push #7074: Pull request #30657 synchronize by alreadydone
35s alreadydone:PicSemiring+
alreadydone:PicSemiring+
35s
chore(without_cdot): remove all uses of without_cdot Run pre-commit and in-place update PR on push #7073: Pull request #30735 opened by JovanGerb
50s JovanGerb:Jovan-without_cdot
JovanGerb:Jovan-without_cdot
50s
feat(gcongr): support @[gcongr] for Monotone and friends Run pre-commit and in-place update PR on push #7072: Pull request #28339 synchronize by JovanGerb
27s JovanGerb:Jovan-gcongr-Monotone
JovanGerb:Jovan-gcongr-Monotone
27s
chore: remove redundant fields from instances Run pre-commit and in-place update PR on push #7071: Pull request #30734 synchronize by JovanGerb
32s JovanGerb:Jovan-remove_instance_fields
JovanGerb:Jovan-remove_instance_fields
32s
doc: fix recurring instances of "this files" Run pre-commit and in-place update PR on push #7070: Pull request #30719 synchronize by harahu
34s harahu:doc/this-files
harahu:doc/this-files
34s
chore(Analysis/CStarAlgebra/CFC/Order): relate section to strict positivity Run pre-commit and in-place update PR on push #7069: Pull request #30694 synchronize by themathqueen
38s themathqueen:todo_posdef
themathqueen:todo_posdef
38s
chore: tidy various files Run pre-commit and in-place update PR on push #7068: Commit 451499a pushed by Ruben-VandeVelde
40s various-tidy-3
various-tidy-3
40s
feat(Geometry/Euclidean/Angle/Unoriented): triangle inequality for angles Run pre-commit and in-place update PR on push #7067: Pull request #26129 synchronize by LessnessRandomness
44s LessnessRandomness:triangle_theorem_for_angles
LessnessRandomness:triangle_theorem_for_angles
44s
chore: remove redundant fields from instances Run pre-commit and in-place update PR on push #7066: Pull request #30734 synchronize by JovanGerb
34s JovanGerb:Jovan-remove_instance_fields
JovanGerb:Jovan-remove_instance_fields
34s
feat(gcongr): support @[gcongr] for Monotone and friends Run pre-commit and in-place update PR on push #7065: Pull request #28339 synchronize by JovanGerb
53s JovanGerb:Jovan-gcongr-Monotone
JovanGerb:Jovan-gcongr-Monotone
53s
doc: fix recurring instances of "this files" Run pre-commit and in-place update PR on push #7064: Pull request #30719 synchronize by harahu
23s harahu:doc/this-files
harahu:doc/this-files
23s
feat(Geometry/Euclidean/Projection): projection onto sup Run pre-commit and in-place update PR on push #7063: Pull request #30703 synchronize by jsm28
33s jsm28:orthogonalProjection_sup_of_orthogonalProjection_eq
jsm28:orthogonalProjection_sup_of_orthogonalProjection_eq
33s
[Merged by Bors] - feat(LinearAlgebra/AffineSpace/AffineSubspace/Defs): nonempty sup Run pre-commit and in-place update PR on push #7062: Pull request #30699 synchronize by jsm28
33s jsm28:AffineSubspace_nonempty_sup
jsm28:AffineSubspace_nonempty_sup
33s
feat(MeasureTheory): add MemLp.Const class and instances to unify p = ∞ and μ.IsFiniteMeasure cases Run pre-commit and in-place update PR on push #7061: Pull request #30030 synchronize by JonBannon
32s JonBannon:MemLp_Const
JonBannon:MemLp_Const
32s
chore: rename field inf to min in Lattice Run pre-commit and in-place update PR on push #7060: Pull request #24614 synchronize by JovanGerb
25s Jovan-inf-min
Jovan-inf-min
25s
fixes Run pre-commit and in-place update PR on push #7059: Commit fb6aacd pushed by JovanGerb
36s Jovan-inf-min
Jovan-inf-min
36s