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,641 workflow runs
1,641 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
feat(Combinatorics/SimpleGraph/Hamiltonian): a graph with a Hamiltoni… Run pre-commit and in-place update PR on push #1616: Commit 57c56e9 pushed by SnirBroshi
33s feature/simple-graph/hamiltonian/small-lemmas
feature/simple-graph/hamiltonian/small-lemmas
33s
more path lemmas Run pre-commit and in-place update PR on push #1615: Commit fb3e2fd pushed by SnirBroshi
22s feature/simple-graph/walk/iscycle-iff-droplast-ispath
feature/simple-graph/walk/iscycle-iff-droplast-ispath
22s
feat(Combinatorics/SimpleGraph/Paths): `p.IsCycle ↔ p.dropLast.IsPath… Run pre-commit and in-place update PR on push #1614: Commit 8b9033a pushed by SnirBroshi
27s feature/simple-graph/walk/iscycle-iff-droplast-ispath
feature/simple-graph/walk/iscycle-iff-droplast-ispath
27s
fix Subgraph.lean Run pre-commit and in-place update PR on push #1613: Commit 7a685a6 pushed by SnirBroshi
29s chore/simple-graph/paths-spell-iic
chore/simple-graph/paths-spell-iic
29s
rewrite IsPath.getVert_injOn Run pre-commit and in-place update PR on push #1612: Commit e80d61a pushed by SnirBroshi
28s chore/simple-graph/paths-spell-iic
chore/simple-graph/paths-spell-iic
28s
Merge branch 'master' into chore/set/reduce-defeq/basics Run pre-commit and in-place update PR on push #1611: Commit 300c9b5 pushed by SnirBroshi
29s chore/set/reduce-defeq/basics
chore/set/reduce-defeq/basics
29s
feat(Combinatorics/SimpleGraph/Hamiltonian): a graph is Hamiltonian i… Run pre-commit and in-place update PR on push #1610: Commit f89dabe pushed by SnirBroshi
30s feature/simple-graph/fancy-hamiltonian-lemmas
feature/simple-graph/fancy-hamiltonian-lemmas
30s
remove isUnit_iff_forall_map_eq_zero Run pre-commit and in-place update PR on push #1609: Commit 6bdb864 pushed by SnirBroshi
27s feature/matrix/mem-spectrum-iff-mulvec
feature/matrix/mem-spectrum-iff-mulvec
27s
feat(Combinatorics/SimpleGraph/Girth): egirth and `(cycleGraph n).F… Run pre-commit and in-place update PR on push #1608: Commit 3ef526a pushed by SnirBroshi
25s feature/simple-graph/egirth-cyclegraph
feature/simple-graph/egirth-cyclegraph
25s
feat(Combinatorics/SimpleGraph/Girth): relate girth and egirth Run pre-commit and in-place update PR on push #1607: Commit d306712 pushed by SnirBroshi
27s feature/simple-graph/girth-egirth
feature/simple-graph/girth-egirth
27s
chore(SimpleGraph/Girth): namespace egirth_le_length under IsCycle Run pre-commit and in-place update PR on push #1606: Commit 330cb1d pushed by SnirBroshi
29s chore/simple-graph/rename-girth-le-length
chore/simple-graph/rename-girth-le-length
29s
feat(SimpleGraph): some CliqueFree/Free lemmas Run pre-commit and in-place update PR on push #1605: Commit ed048d6 pushed by SnirBroshi
30s feature/simple-graph/clique-free-lemmas
feature/simple-graph/clique-free-lemmas
30s
add CliqueFree.free_top_fin alias Run pre-commit and in-place update PR on push #1604: Commit 39aca49 pushed by SnirBroshi
21s chore/simple-graph/clique-free-iff-cleanup
chore/simple-graph/clique-free-iff-cleanup
21s
feat(Data/ENat/Basic): coe versions of m + 1 ≤ n ↔ m < n Run pre-commit and in-place update PR on push #1603: Commit 4611423 pushed by SnirBroshi
32s feature/data/enat-succ-le-lt-iff-coe
feature/data/enat-succ-le-lt-iff-coe
32s
golf the other ENat theorem Run pre-commit and in-place update PR on push #1602: Commit af073fe pushed by SnirBroshi
22s feature/order/succ-le-lt-ismax
feature/order/succ-le-lt-ismax
22s
feat(Order/SuccPred): succ a ≤ b ↔ a < b when b is not maximal Run pre-commit and in-place update PR on push #1601: Commit 9882f30 pushed by SnirBroshi
27s feature/order/succ-le-lt-ismax
feature/order/succ-le-lt-ismax
27s
i forgot this pr has a better IsAcyclic.cliqueFree Run pre-commit and in-place update PR on push #1600: Commit ab67212 pushed by SnirBroshi
23s feature/simple-graph/star-triangle-free
feature/simple-graph/star-triangle-free
23s
chore(SimpleGraph/Clique): tidy CliqueFree iff lemmas Run pre-commit and in-place update PR on push #1599: Commit 09be106 pushed by SnirBroshi
31s chore/simple-graph/clique-free-iff-cleanup
chore/simple-graph/clique-free-iff-cleanup
31s
feat(SimpleGraph/Acyclic): a graph is acyclic iff it is free of cycle… Run pre-commit and in-place update PR on push #1598: Commit 14da713 pushed by SnirBroshi
26s feature/simple-graph/acyclic-iff-cycle-free
feature/simple-graph/acyclic-iff-cycle-free
26s
empty commit to retrigger CI Run pre-commit and in-place update PR on push #1597: Commit 93a25ff pushed by SnirBroshi
23s feature/order/relation-map-onfun-morphisms
feature/order/relation-map-onfun-morphisms
23s
remove mem_spectrum_iff_exists_map_eq_smul which combines two lemmas Run pre-commit and in-place update PR on push #1596: Commit 945925b pushed by SnirBroshi
22s feature/matrix/mem-spectrum-iff-mulvec
feature/matrix/mem-spectrum-iff-mulvec
22s
add EquivLike.toEquiv lemmas for the RelIso defs Run pre-commit and in-place update PR on push #1595: Commit a53c991 pushed by SnirBroshi
28s feature/order/relation-map-onfun-morphisms
feature/order/relation-map-onfun-morphisms
28s
chore(Combinatorics/SimpleGraph/Girth): golf egirth_top using `cycl… Run pre-commit and in-place update PR on push #1594: Commit e4932f2 pushed by SnirBroshi
32s golf/simple-graph/egirth-top
golf/simple-graph/egirth-top
32s
feat(Combinatorics/SimpleGraph/Subgraph): induce lemmas Run pre-commit and in-place update PR on push #1593: Commit bfcecc9 pushed by SnirBroshi
27s feature/simple-graph/subgraph-induce-lemmas
feature/simple-graph/subgraph-induce-lemmas
27s
s.sup zmultiples = closure s in any additive subgroup Run pre-commit and in-place update PR on push #1592: Commit 59cb914 pushed by SnirBroshi
29s feature/group-theory/zmultiples-int-finset
feature/group-theory/zmultiples-int-finset
29s