Skip to content

Actions: Deep0Thinking/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
105 workflow runs
105 workflow runs

Filter by Event

⌥ + click/return to exclude

Filter by Status

⌥ + click/return to exclude

Filter by Branch

⌥ + click/return to exclude

Filter by Actor

⌥ + click/return to exclude
Merge branch 'master' into Frullani_integral Run pre-commit and in-place update PR on push #80: Commit 9d3d5b1 pushed by Deep0Thinking
21s Frullani_integral
Frullani_integral
21s
Merge branch 'master' into Frullani_integral Run pre-commit and in-place update PR on push #79: Commit 95ec31c pushed by Deep0Thinking
22s Frullani_integral
Frullani_integral
22s
docs(Analysis/SpecialFunctions/ImproperIntegrals): update authorship Run pre-commit and in-place update PR on push #78: Commit 6be25c3 pushed by Deep0Thinking
21s Frullani_integral
Frullani_integral
21s
Merge branch 'master' into Frullani_integral Run pre-commit and in-place update PR on push #77: Commit 95ec31c pushed by Deep0Thinking
25s Frullani_integral
Frullani_integral
25s
fix(Combinatorics/Enumerative/Bonferroni): make "Bonferroni.lean" a m… Run pre-commit and in-place update PR on push #76: Commit 5bb521a pushed by Deep0Thinking
1m 36s bonferroni-inclusion-exclusion
bonferroni-inclusion-exclusion
1m 36s
chore: regenerate Mathlib.lean with mk_all Run pre-commit and in-place update PR on push #75: Commit ae51ff5 pushed by Deep0Thinking
27s bonferroni-inclusion-exclusion
bonferroni-inclusion-exclusion
27s
style(Combinatorics/Enumerative/Bonferroni): fix linter warning Run pre-commit and in-place update PR on push #74: Commit a564e38 pushed by Deep0Thinking
21s bonferroni-inclusion-exclusion
bonferroni-inclusion-exclusion
21s
chore(Combinatorics/Enumerative/InclusionExclusion): remove solved TODO Run pre-commit and in-place update PR on push #73: Commit e503193 pushed by Deep0Thinking
23s bonferroni-inclusion-exclusion
bonferroni-inclusion-exclusion
23s
feat(Combinatorics/Enumerative/Bonferroni): add Bonferroni inequalities Run pre-commit and in-place update PR on push #72: Commit b16b285 pushed by Deep0Thinking
22s bonferroni-inclusion-exclusion
bonferroni-inclusion-exclusion
22s
chore: change remaining _neq_ to _ne_ (#35350) Run pre-commit and in-place update PR on push #71: Commit 1757879 pushed by Deep0Thinking
29s bonferroni-inclusion-exclusion
bonferroni-inclusion-exclusion
29s
refactor(MeasureTheory/Integral/DominatedConvergence): golf and format Run pre-commit and in-place update PR on push #70: Commit acada00 pushed by Deep0Thinking
29s tendsto_integral_Ioi
tendsto_integral_Ioi
29s
refactor(MeasureTheory/Integral/DominatedConvergence): remove redunda… Run pre-commit and in-place update PR on push #69: Commit 455228b pushed by Deep0Thinking
24s tendsto_integral_Ioi
tendsto_integral_Ioi
24s
refactor(MeasureTheory/Integral/IntervalIntegral/Basic): remove hypot… Run pre-commit and in-place update PR on push #68: Commit 0470b66 pushed by Deep0Thinking
27s tendsto_integral_Ioi
tendsto_integral_Ioi
27s
feat(MeasureTheory/Integral/Bochner/Set): add `integral_Ico_eq_integr… Run pre-commit and in-place update PR on push #67: Commit 976461b pushed by Deep0Thinking
24s tendsto_integral_Ioi
tendsto_integral_Ioi
24s
refactor(Order/Interval/Set/LinearOrder): golf Ioi_diff_Ioc using `… Run pre-commit and in-place update PR on push #66: Commit 58f09da pushed by Deep0Thinking
24s tendsto_integral_Ioi
tendsto_integral_Ioi
24s
refactor(Analysis/Calculus/DerivativeTest): generalize and clean up Run pre-commit and in-place update PR on push #65: Commit 30e1942 pushed by Deep0Thinking
26s derivativetest
derivativetest
26s
Merge pull request #1 from Deep0Thinking/derivativetest Run pre-commit and in-place update PR on push #64: Commit c326ec3 pushed by Deep0Thinking
21s derivativetest
derivativetest
21s
refactor(Analysis/Calculus/DerivativeTest): generalize and clean up Run pre-commit and in-place update PR on push #63: Commit 981069b pushed by Deep0Thinking
30s derivativetest
derivativetest
30s
style(Analysis/Calculus/DerivativeTest): format Run pre-commit and in-place update PR on push #62: Commit 4d2f8d1 pushed by Deep0Thinking
27s derivativetest
derivativetest
27s
style(Analysis/Calculus/DerivativeTest): format Run pre-commit and in-place update PR on push #61: Commit b66e4fa pushed by Deep0Thinking
24s derivativetest
derivativetest
24s
feat(Analysis/Calculus/DerivativeTest): add continuousOn_*, `isMaxO… Run pre-commit and in-place update PR on push #60: Commit 5b5db12 pushed by Deep0Thinking
25s derivativetest
derivativetest
25s
refactor(MeasureTheory/Integral/DominatedConvergence): rename theorem… Run pre-commit and in-place update PR on push #59: Commit c616426 pushed by Deep0Thinking
25s tendsto_integral_Ioi
tendsto_integral_Ioi
25s
chore(MeasureTheory/Integral/IntegralEqImproper): remove redundant im… Run pre-commit and in-place update PR on push #58: Commit 2e28db1 pushed by Deep0Thinking
24s tendsto_integral_Ioi
tendsto_integral_Ioi
24s
refactor(MeasureTheory/Integral/DominatedConvergence): golf; improve … Run pre-commit and in-place update PR on push #57: Commit 56267c9 pushed by Deep0Thinking
24s tendsto_integral_Ioi
tendsto_integral_Ioi
24s
feat(MeasureTheory/Integral/IntervalIntegral/Basic): add `integral_Io… Run pre-commit and in-place update PR on push #56: Commit 1aaeb22 pushed by Deep0Thinking
26s tendsto_integral_Ioi
tendsto_integral_Ioi
26s