Skip to content
continuous integration (staging)

feat: add a few lemmas about MvPolynomial.totalDegree (#8815) #5566

Sign in to view logs

feat: add a few lemmas about MvPolynomial.totalDegree (#8815)

feat: add a few lemmas about MvPolynomial.totalDegree (#8815) #5566

Triggered via push December 4, 2023 19:59
@mathlib-borsmathlib-bors[bot]
pushed b336016
staging
Status Cancelled
Total duration 1m 28s
Artifacts –

bors.yml

on: push
Lint style
33s
Lint style
Check all files imported
9s
Check all files imported
Build
1m 19s
Build
Cancel Previous Runs (CI)
5s
Cancel Previous Runs (CI)
check workflows
9s
check workflows
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

5 errors
Lint style: Mathlib/RingTheory/PolynomialAlgebra.lean#L106
Mathlib/RingTheory/PolynomialAlgebra.lean#L106: ERR_ARR: Missing space after '←'.
Lint style: Mathlib/RingTheory/PolynomialAlgebra.lean#L107
Mathlib/RingTheory/PolynomialAlgebra.lean#L107: ERR_ARR: Missing space after '←'.
Lint style
Process completed with exit code 123.
Build
The run was canceled by @github-actions.
Build
The operation was canceled.