Skip to content

Actions: daniel-carranza/mathlib4

Actions

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

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
21 workflow runs
21 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
fix the build Run pre-commit and in-place update PR on push #21: Commit e556b82 pushed by dagurtomas
29s internal-currying-isomorphism
internal-currying-isomorphism
29s
Merge branch 'master' into internal-currying-isomorphism Run pre-commit and in-place update PR on push #20: Commit 7420d6c pushed by dagurtomas
37s internal-currying-isomorphism
internal-currying-isomorphism
37s
Update Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean Run pre-commit and in-place update PR on push #19: Commit ee7b613 pushed by daniel-carranza
48s internal-currying-isomorphism
internal-currying-isomorphism
48s
corrected TODO comments Run pre-commit and in-place update PR on push #18: Commit 355de62 pushed by daniel-carranza
30s internal-currying-isomorphism
internal-currying-isomorphism
30s
trying to resolve merge conflicts Run pre-commit and in-place update PR on push #17: Commit 041cf6a pushed by daniel-carranza
22s internal-currying-isomorphism
internal-currying-isomorphism
22s
Update Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean Run pre-commit and in-place update PR on push #16: Commit f74aab5 pushed by daniel-carranza
23s internal-currying-isomorphism
internal-currying-isomorphism
23s
Update Mathlib/CategoryTheory/Monoidal/Closed/InternalCurrying.lean Run pre-commit and in-place update PR on push #15: Commit c732b49 pushed by daniel-carranza
20s internal-currying-isomorphism
internal-currying-isomorphism
20s
removed reverseBraiding from file Run pre-commit and in-place update PR on push #14: Commit eec6fd0 pushed by daniel-carranza
33s enriched-cotensors
enriched-cotensors
33s
added reassoc and simp to uncurry_curry and curry_uncurry lemmas Run pre-commit and in-place update PR on push #13: Commit fb7225b pushed by daniel-carranza
28s internal-currying-isomorphism
internal-currying-isomorphism
28s
added additional "end" Run pre-commit and in-place update PR on push #12: Commit 5f0b942 pushed by daniel-carranza
29s internal-currying-isomorphism
internal-currying-isomorphism
29s
added @[expose] at start of section; added @[simps] to the isomorphism Run pre-commit and in-place update PR on push #11: Commit b0d59a0 pushed by daniel-carranza
20s internal-currying-isomorphism
internal-currying-isomorphism
20s
updated file to import InternalCurrying.lean Run pre-commit and in-place update PR on push #10: Commit 9c7d1a8 pushed by daniel-carranza
25s enriched-cotensors
enriched-cotensors
25s
added InternalCurrying file to Mathlib.lean Run pre-commit and in-place update PR on push #9: Commit 8b8c608 pushed by daniel-carranza
29s internal-currying-isomorphism
internal-currying-isomorphism
29s
added line which construct the cotensor as functor out of the product Run pre-commit and in-place update PR on push #8: Commit 570a47c pushed by daniel-carranza
36s enriched-cotensors
enriched-cotensors
36s
added new file to Mathlib.lean Run pre-commit and in-place update PR on push #7: Commit c5939f5 pushed by daniel-carranza
25s enriched-cotensors
enriched-cotensors
25s
removed @[reassoc] tag from lemmas without any composition Run pre-commit and in-place update PR on push #6: Commit 71d2b95 pushed by daniel-carranza
27s enriched-product-category
enriched-product-category
27s
removed simp tag from lemmas whose LHS are not in simp normal form. Run pre-commit and in-place update PR on push #5: Commit 275b57d pushed by daniel-carranza
26s enriched-product-category
enriched-product-category
26s
added @[simps] tag to tensor\mu_iso (implementing commit suggestion) Run pre-commit and in-place update PR on push #4: Commit 34c983a pushed by daniel-carranza
30s enriched-product-category
enriched-product-category
30s
added some missing docstrings Run pre-commit and in-place update PR on push #3: Commit 8de88bd pushed by daniel-carranza
24s enriched-product-category
enriched-product-category
24s
removed redundant call to exact, changed a terminal simp (1 remaining) Run pre-commit and in-place update PR on push #2: Commit 8459d29 pushed by daniel-carranza
23s enriched-product-category
enriched-product-category
23s
add new file on tensor product of V-categories Run pre-commit and in-place update PR on push #1: Commit e6c3350 pushed by daniel-carranza
29s enriched-product-category
enriched-product-category
29s