Skip to content

Actions: SnirBroshi/mathlib4

Actions

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

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
1,678 workflow runs
1,678 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
chore(Data/List/Nodup): golf nodup_iff_injective_get Run pre-commit and in-place update PR on push #103: Commit a656988 pushed by SnirBroshi
33s chore/golf-list-nodup-iff-injective-get
chore/golf-list-nodup-iff-injective-get
33s
feat(Combinatorics/SimpleGraph/Paths): path iff p.support.get is in… Run pre-commit and in-place update PR on push #102: Commit c2105b8 pushed by SnirBroshi
23s feature/path-support-get-injective
feature/path-support-get-injective
23s
feat(Combinatorics/SimpleGraph/Paths): path iff p.support.get is in… Run pre-commit and in-place update PR on push #101: Commit 8293562 pushed by SnirBroshi
22s feature/path-support-get-injective
feature/path-support-get-injective
22s
feat(Data/List/GetD): getD is surjective iff every element is in th… Run pre-commit and in-place update PR on push #100: Commit c1e13a9 pushed by SnirBroshi
23s feature/list-getd-surjective
feature/list-getd-surjective
23s
feat(Data/List/Basic): get is surjective iff every element is in th… Run pre-commit and in-place update PR on push #99: Commit b552d13 pushed by SnirBroshi
23s feature/list-get-surjective
feature/list-get-surjective
23s
feat(Combinatorics/SimpleGraph/Hamiltonian): p.support.get and `p.g… Run pre-commit and in-place update PR on push #98: Commit 2d278af pushed by SnirBroshi
24s feature/hamiltonian-equiv-fin
feature/hamiltonian-equiv-fin
24s
feat(Data/List/NodupEquivFin): add equiv with count = 1 hypothesis Run pre-commit and in-place update PR on push #97: Commit cec5e84 pushed by SnirBroshi
25s feature/list-equiv-count-eq-one
feature/list-equiv-count-eq-one
25s
feat(Data/List/Basic): add Fin variants of *mem_iff_getElem Run pre-commit and in-place update PR on push #96: Commit f0ee51a pushed by SnirBroshi
26s feature/list-mem-iff-fin
feature/list-mem-iff-fin
26s
feat(Data/List/GetD): golf and add lemmas for get and getElem? Run pre-commit and in-place update PR on push #95: Commit 2f6bd4e pushed by SnirBroshi
27s feature/list-getd-eq-get
feature/list-getd-eq-get
27s
feat(Combinators/SimpleGraph/Hamiltonian): `p.support.length = Fintyp… Run pre-commit and in-place update PR on push #94: Commit 71d2265 pushed by SnirBroshi
29s feature/hamiltonian-length
feature/hamiltonian-length
29s
feat(Combinators/SimpleGraph/Walk): p.getVert is p.support.get Run pre-commit and in-place update PR on push #93: Commit 18c81cd pushed by SnirBroshi
25s feature/walk-getvert-eq-support-get
feature/walk-getvert-eq-support-get
25s
chore(Algebra/BigOperators/Intervals): move `Finset.prod_range_add_on… Run pre-commit and in-place update PR on push #92: Commit 603dcd5 pushed by SnirBroshi
23s chore/factorial-big-operators
chore/factorial-big-operators
23s
feat(Data/Set/Lattice): useful equivalences of biUnion and biInter Run pre-commit and in-place update PR on push #91: Commit bd5439c pushed by SnirBroshi
28s feature/lattice-bi-union-lemmas
feature/lattice-bi-union-lemmas
28s
feat(NumberTheory/ArithmeticFunction): Nat.sum_divisors for sigma… Run pre-commit and in-place update PR on push #90: Commit f5686d3 pushed by SnirBroshi
23s feature/arithmetic-function-lemmas
feature/arithmetic-function-lemmas
23s
feat(FieldTheory/IsSepClosed): generalize exists_aeval_eq_zero from… Run pre-commit and in-place update PR on push #89: Commit b4b597f pushed by SnirBroshi
26s feature/polynomial-lemmas
feature/polynomial-lemmas
26s
feat(Analysis/SpecificLimits/Fibonacci): prove that the ratio of cons… Run pre-commit and in-place update PR on push #88: Commit 8eef535 pushed by SnirBroshi
34s feature/fibonacci-div-limit
feature/fibonacci-div-limit
34s
feat(RingTheory/RootsOfUnity/Complex): exp(pi * i * q) is a root of u… Run pre-commit and in-place update PR on push #87: Commit fdd1b31 pushed by SnirBroshi
25s feature/primitive-root-exp-rat
feature/primitive-root-exp-rat
25s
feat(Data/Seq/Basic): prove basic theorems about Seq.subsequence Run pre-commit and in-place update PR on push #86: Commit 56ed77d pushed by SnirBroshi
35s feature/seq-subsequence
feature/seq-subsequence
35s
feat(Counterexamples): Euler's sum of powers conjecture Run pre-commit and in-place update PR on push #85: Commit 4d882be pushed by SnirBroshi
29s feature/counterexample-euler-sum-of-powers
feature/counterexample-euler-sum-of-powers
29s
feat(Data/Setoid/Basic): add theorems about lifting a function to its… Run pre-commit and in-place update PR on push #84: Commit ec37b92 pushed by SnirBroshi
29s feature/ker-lift
feature/ker-lift
29s
feat(Combinatorics/SimpleGraph/Connectivity): a graph is either conne… Run pre-commit and in-place update PR on push #83: Commit 4aafaf5 pushed by SnirBroshi
32s feature/graph-connected-or-compl-connected
feature/graph-connected-or-compl-connected
32s
feat(Combinatorics/SimpleGraph/Acyclic): a tree is a minimal connecte… Run pre-commit and in-place update PR on push #82: Commit ab14c29 pushed by SnirBroshi
22s feature/tree-iff-minimal-connected
feature/tree-iff-minimal-connected
22s
chore(Mathlib/Order/BooleanAlgebra/Basic): golf rewrites Run pre-commit and in-place update PR on push #81: Commit f10be95 pushed by SnirBroshi
27s chore/golf-order-boolean-algebra-basic
chore/golf-order-boolean-algebra-basic
27s
feat(Logic/Relation): lemmas relating Relation.Map and `Function.on… Run pre-commit and in-place update PR on push #80: Commit cd646f3 pushed by SnirBroshi
29s feature/relation-map-onfun
feature/relation-map-onfun
29s
feat(Logic/Relation): lemmas relating Relation.Map and `Function.on… Run pre-commit and in-place update PR on push #79: Commit 004f3dc pushed by SnirBroshi
27s feature/relation-map-onfun
feature/relation-map-onfun
27s
ProTip! You can narrow down the results and go further in time using created:<2025-10-10 or the other filters available.