Skip to content

Actions: themathqueen/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
1,644 workflow runs
1,644 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
review Run pre-commit and in-place update PR on push #1645: Commit cc48210 pushed by themathqueen
22s mv_lie_toMatrix
mv_lie_toMatrix
22s
Merge branch 'master' into mv_lie_toMatrix Run pre-commit and in-place update PR on push #1644: Commit 77f96f7 pushed by themathqueen
27s mv_lie_toMatrix
mv_lie_toMatrix
27s
use simp instead Run pre-commit and in-place update PR on push #1643: Commit 4d50ddb pushed by themathqueen
53s mv_lie_toMatrix
mv_lie_toMatrix
53s
maybe revert Run pre-commit and in-place update PR on push #1642: Commit 5866495 pushed by themathqueen
25s mv_lie_toMatrix
mv_lie_toMatrix
25s
move LIE.toMatri_mem_unitaryGroup to PiL2 Run pre-commit and in-place update PR on push #1641: Commit 428bb8a pushed by themathqueen
30s mv_lie_toMatrix
mv_lie_toMatrix
30s
Update Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean Run pre-commit and in-place update PR on push #1640: Commit db75e19 pushed by themathqueen
25s refactor_orthoProj
refactor_orthoProj
25s
no need for set_option Run pre-commit and in-place update PR on push #1639: Commit 025e7ef pushed by themathqueen
31s refactor_orthoProj
refactor_orthoProj
31s
update message Run pre-commit and in-place update PR on push #1638: Commit 0aa6844 pushed by themathqueen
21s refactor_orthoProj
refactor_orthoProj
21s
i think i added them all back Run pre-commit and in-place update PR on push #1637: Commit 2876a32 pushed by themathqueen
25s refactor_orthoProj
refactor_orthoProj
25s
Apply suggestions from code review Run pre-commit and in-place update PR on push #1636: Commit b046924 pushed by themathqueen
29s refactor_orthoProj
refactor_orthoProj
29s
revert coercions Run pre-commit and in-place update PR on push #1635: Commit d1bbd8c pushed by themathqueen
25s tensorProduct_mkL
tensorProduct_mkL
25s
ridIsometry and more API Run pre-commit and in-place update PR on push #1634: Commit ed7e4e4 pushed by themathqueen
30s tensorProduct_mkL
tensorProduct_mkL
30s
Merge branch 'master' into tensorProduct_mkL Run pre-commit and in-place update PR on push #1633: Commit 202629e pushed by themathqueen
24s tensorProduct_mkL
tensorProduct_mkL
24s
Merge branch 'master' into tensorProduct_inner_def Run pre-commit and in-place update PR on push #1632: Commit e4dde51 pushed by themathqueen
23s tensorProduct_inner_def
tensorProduct_inner_def
23s
style Run pre-commit and in-place update PR on push #1631: Commit 3c128ae pushed by themathqueen
28s tensorProduct_inner_def
tensorProduct_inner_def
28s
revert Run pre-commit and in-place update PR on push #1630: Commit c81bf7a pushed by themathqueen
26s tensorProduct_inner_def
tensorProduct_inner_def
26s
remove doc Run pre-commit and in-place update PR on push #1629: Commit 89b4252 pushed by themathqueen
20s tensorProduct_inner_def
tensorProduct_inner_def
20s
remove private inner_ def Run pre-commit and in-place update PR on push #1628: Commit 0910e35 pushed by themathqueen
39s tensorProduct_inner_def
tensorProduct_inner_def
39s
two more Run pre-commit and in-place update PR on push #1627: Commit 5da0c42 pushed by themathqueen
28s tensorProduct_mkL
tensorProduct_mkL
28s
add coe_mkL_apply and make that simp instead Run pre-commit and in-place update PR on push #1626: Commit f824c42 pushed by themathqueen
20s tensorProduct_mkL
tensorProduct_mkL
20s
mkL Run pre-commit and in-place update PR on push #1625: Commit a98359d pushed by themathqueen
29s tensorProduct_mkL
tensorProduct_mkL
29s
instead of alias Run pre-commit and in-place update PR on push #1624: Commit 960b1d8 pushed by themathqueen
27s refactor_orthoProj
refactor_orthoProj
27s
fix Run pre-commit and in-place update PR on push #1623: Commit 249c341 pushed by themathqueen
28s refactor_orthoProj
refactor_orthoProj
28s
remove duplicate Run pre-commit and in-place update PR on push #1622: Commit a01d2ef pushed by themathqueen
26s refactor_orthoProj
refactor_orthoProj
26s
remove the Fn lemmas and defs Run pre-commit and in-place update PR on push #1621: Commit ff14157 pushed by themathqueen
45s refactor_orthoProj
refactor_orthoProj
45s