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
|
build mathlib:
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L263
unknown identifier 'N'
|
|
build mathlib:
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L263
application type mismatch
|
|
build mathlib:
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L265
application type mismatch
|
|
build mathlib:
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L265
unknown identifier 'N'
|
|
build mathlib:
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L321
unknown identifier 'N'
|
|
build mathlib:
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L322
application type mismatch
|
|
build mathlib:
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L323
application type mismatch
|
|
build mathlib:
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L328
unknown identifier 'N'
|
|
build mathlib:
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L329
application type mismatch
|
|
build mathlib:
Mathlib/LinearAlgebra/Multilinear/Basic.lean#L329
application type mismatch
|
The logs for this run have expired and are no longer available.
Loading