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
Annotations
10 errors
|
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 `|`)
|
|
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 `|`)
|
|
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 `|`)
|
|
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L258
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L258: ERR_LIN: Line has more than 100 characters
|
|
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L260
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L260: ERR_LIN: Line has more than 100 characters
|
|
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L261
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L261: ERR_LIN: Line has more than 100 characters
|
|
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L293
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L293: ERR_LIN: Line has more than 100 characters
|
|
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L354
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L354: ERR_LIN: Line has more than 100 characters
|
|
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L431
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L431: ERR_LIN: Line has more than 100 characters
|
|
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L273
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L273: ERR_DOT: Line is an isolated focusing dot or uses . instead of ·
|
The logs for this run have expired and are no longer available.
Loading