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,229 workflow runs
7,229 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

feat(Nat/Nth): inequalities about Nat.nth Run pre-commit and in-place update PR on push #7104: Pull request #27742 synchronize by ChrisHughes24
32s ChrisHughes24:nth_lemmas
ChrisHughes24:nth_lemmas
32s
fix(gcongr): use whnfR on the sides of the relation Run pre-commit and in-place update PR on push #7103: Pull request #30741 synchronize by JovanGerb
32s JovanGerb:Jovan-gcongr-whnf
JovanGerb:Jovan-gcongr-whnf
32s
refactor(Analysis/NormedSpace/Exponential): remove the 𝕂 argument from exp Run pre-commit and in-place update PR on push #7102: Pull request #30706 synchronize by astrainfinita
31s astrainfinita:exp_rat_junkvalue
astrainfinita:exp_rat_junkvalue
31s
feat: elementary lemmas aiding computations with log⁺, Mark II Run pre-commit and in-place update PR on push #7101: Pull request #30729 synchronize by kebekus
35s kebekus:kebekus/posLog3
kebekus:kebekus/posLog3
35s
refactor(Analysis/NormedSpace/Exponential): remove the 𝕂 argument from exp Run pre-commit and in-place update PR on push #7100: Pull request #30706 synchronize by astrainfinita
30s astrainfinita:exp_rat_junkvalue
astrainfinita:exp_rat_junkvalue
30s
feat: elementary lemmas aiding computations with log⁺, Mark II Run pre-commit and in-place update PR on push #7099: Pull request #30729 synchronize by kebekus
42s kebekus:kebekus/posLog3
kebekus:kebekus/posLog3
42s
fix(gcongr): use whnfR on the sides of the relation Run pre-commit and in-place update PR on push #7098: Pull request #30741 opened by JovanGerb
35s JovanGerb:Jovan-gcongr-whnf
JovanGerb:Jovan-gcongr-whnf
35s
chore: merge bump/v4.25.0 Run pre-commit and in-place update PR on push #7097: Pull request #30740 opened by kim-em
32s leanprover-community:bump/v4.25.0
leanprover-community:bump/v4.25.0
32s
refactor(Analysis/NormedSpace/Exponential): remove the 𝕂 argument from exp Run pre-commit and in-place update PR on push #7096: Pull request #30706 synchronize by astrainfinita
37s astrainfinita:exp_rat_junkvalue
astrainfinita:exp_rat_junkvalue
37s
feat(gcongr): use mdata instead of template Run pre-commit and in-place update PR on push #7095: Pull request #30739 opened by JovanGerb
32s JovanGerb:Jovan-gcongr-mdata
JovanGerb:Jovan-gcongr-mdata
32s
feat(Data/Finset/Card): add some more Pigeonhole Principle theorems exists_ne_map_eq_of_card_image_lt and not_injOn_of_card_image_lt Run pre-commit and in-place update PR on push #7094: Pull request #28077 synchronize by ShreckYe
42s ShreckYe:pigeonhole-principle-finset-exists_ne_map_eq_of_card_image_lt
ShreckYe:pigeonhole-principle-finset-exists_ne_map_eq_of_card_image_lt
42s
feat(Homology) : Ext commute with flat base change Run pre-commit and in-place update PR on push #7093: Pull request #30532 synchronize by Thmoas-Guan
28s Thmoas-Guan:Ext-Base-Change
Thmoas-Guan:Ext-Base-Change
28s
feat(MeasureTheory): add MemLp.Const class and instances to unify p = ∞ and μ.IsFiniteMeasure cases Run pre-commit and in-place update PR on push #7092: Pull request #30030 synchronize by JonBannon
33s JonBannon:MemLp_Const
JonBannon:MemLp_Const
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 #7091: Pull request #30030 synchronize by JonBannon
34s JonBannon:MemLp_Const
JonBannon:MemLp_Const
34s
feat(FieldTheory): construct extension of finite field Run pre-commit and in-place update PR on push #7090: Pull request #30738 synchronize by kckennylau
26s kckennylau:finite-field-extension
kckennylau:finite-field-extension
26s
feat(FieldTheory): construct extension of finite field Run pre-commit and in-place update PR on push #7089: Pull request #30738 synchronize by kckennylau
34s kckennylau:finite-field-extension
kckennylau:finite-field-extension
34s
feat(FieldTheory): construct extension of finite field Run pre-commit and in-place update PR on push #7088: Pull request #30738 synchronize by kckennylau
35s kckennylau:finite-field-extension
kckennylau:finite-field-extension
35s
feat(FieldTheory): construct extension of finite field Run pre-commit and in-place update PR on push #7087: Pull request #30738 synchronize by kckennylau
36s kckennylau:finite-field-extension
kckennylau:finite-field-extension
36s
feat(FieldTheory): construct extension of finite field Run pre-commit and in-place update PR on push #7086: Pull request #30738 opened by kckennylau
36s kckennylau:finite-field-extension
kckennylau:finite-field-extension
36s
feat(Algebra/Polynomial/Factors): Introduce predicate and basic API Run pre-commit and in-place update PR on push #7085: Pull request #30212 synchronize by tb65536
29s tb65536:tb_sp
tb65536:tb_sp
29s
feat(gcongr): support @[gcongr] for Monotone and friends Run pre-commit and in-place update PR on push #7084: Pull request #28339 synchronize by JovanGerb
27s JovanGerb:Jovan-gcongr-Monotone
JovanGerb:Jovan-gcongr-Monotone
27s
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
[Merged by Bors] - 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