fixes #165744
Annotations
4 errors and 2 warnings
|
check for unused imports
The process '/usr/bin/env' failed with exit code 1
|
|
lint mathlib:
Mathlib/MeasureTheory/Function/L1Space/Integrable.lean#L433
@MeasureTheory.Integrable.essSup_smul unnecessary have h : 1 /
|
|
lint mathlib:
Mathlib/MeasureTheory/Function/L1Space/Integrable.lean#L449
@MeasureTheory.Integrable.smul_essSup unnecessary have h : 1 /
|
|
lint mathlib
The process '/usr/bin/env' failed with exit code 1
|
|
check for unused imports:
Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean#L9
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
|
check for unused imports:
Mathlib/MeasureTheory/Function/Holder.lean#L8
unused import (use `lake exe shake --fix` to fix this, or `lake exe shake --update` to ignore)
|
Loading