This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Merge remote-tracking branch 'origin/master' into MultilinearMapContDiff #81629
smorel394build_fork.yml
on: push
Lint style (fork)
19s
Check all files imported (fork)
8s
Build (fork)
3m 51s
Cancel Previous Runs (CI)
0s
check workflows (fork)
9s
Post-CI job (fork)
0s
Annotations
20 errors
|
Lint style (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L264
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L264: ERR_IND: If the theorem/def statement requires multiple lines, indent it correctly (4 spaces or 2 for `|`)
|
|
Lint style (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L322
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L322: ERR_IND: If the theorem/def statement requires multiple lines, indent it correctly (4 spaces or 2 for `|`)
|
|
Lint style (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L329
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L329: ERR_IND: If the theorem/def statement requires multiple lines, indent it correctly (4 spaces or 2 for `|`)
|
|
Lint style (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L258
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L258: ERR_LIN: Line has more than 100 characters
|
|
Lint style (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L260
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L260: ERR_LIN: Line has more than 100 characters
|
|
Lint style (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L261
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L261: ERR_LIN: Line has more than 100 characters
|
|
Lint style (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L293
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L293: ERR_LIN: Line has more than 100 characters
|
|
Lint style (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L354
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L354: ERR_LIN: Line has more than 100 characters
|
|
Lint style (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L431
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L431: ERR_LIN: Line has more than 100 characters
|
|
Lint style (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L273
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L273: ERR_DOT: Line is an isolated focusing dot or uses . instead of ·
|
|
Build (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L263
unknown identifier 'N'
|
|
Build (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L263
application type mismatch
|
|
Build (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L265
application type mismatch
|
|
Build (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L265
unknown identifier 'N'
|
|
Build (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L321
unknown identifier 'N'
|
|
Build (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L322
application type mismatch
|
|
Build (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L323
application type mismatch
|
|
Build (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L328
unknown identifier 'N'
|
|
Build (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L329
application type mismatch
|
|
Build (fork):
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L329
application type mismatch
|