Update Mathlib.lean #128967
Annotations
8 errors
|
lint mathlib:
Mathlib/Topology/Algebra/SeparationQuotient.lean#L144
@SeparationQuotient.liftAddMonoidHom definition missing documentation string
|
|
lint mathlib:
Mathlib/Topology/Algebra/SeparationQuotient.lean#L145
@SeparationQuotient.liftMonoidHom definition missing documentation string
|
|
lint mathlib:
Mathlib/Analysis/InnerProductSpace/SeparationQuotient.lean#L33
nullSubmodule should not be an instance
|
|
lint mathlib:
Mathlib/Topology/Algebra/SeparationQuotient.lean#L144
@SeparationQuotient.liftAddMonoidHom argument 8 inst✝ : ContinuousAdd
|
|
lint mathlib:
Mathlib/Topology/Algebra/SeparationQuotient.lean#L145
@SeparationQuotient.liftMonoidHom argument 8 inst✝ : ContinuousMul
|
|
lint mathlib:
Mathlib/Topology/Algebra/SeparationQuotient.lean#L221
@SeparationQuotient.nhds_eq argument 4 inst✝ : TopologicalAddGroup
|
|
lint mathlib
The process '/usr/bin/env' failed with exit code 1
|
|
build mathlib
The process '/usr/bin/bash' failed with exit code 1
|
Loading