Merge remote-tracking branch 'origin' into localization-monoidal #151597
Annotations
11 errors
|
lint mathlib:
Mathlib/CategoryTheory/Localization/Monoidal.lean#L23
@CategoryTheory.MonoidalCategory.Pentagon definition missing documentation string
|
|
lint mathlib:
Mathlib/CategoryTheory/Localization/Monoidal.lean#L34
@CategoryTheory.MorphismProperty.Monoidal inductive missing documentation string
|
|
lint mathlib:
Mathlib/CategoryTheory/Localization/Monoidal.lean#L53
@CategoryTheory.LocalizedMonoidal definition missing documentation string
|
|
lint mathlib:
Mathlib/CategoryTheory/Localization/Monoidal.lean#L67
@CategoryTheory.Localization.Monoidal.toMonoidalCategory definition missing documentation string
|
|
lint mathlib:
Mathlib/CategoryTheory/Localization/Monoidal.lean#L86
@CategoryTheory.Localization.Monoidal.tensorBifunctor definition missing documentation string
|
|
lint mathlib:
Mathlib/CategoryTheory/Localization/Monoidal.lean#L95
CategoryTheory.Localization.Monoidal.whiskeringRight₂' definition missing documentation string
|
|
lint mathlib:
Mathlib/CategoryTheory/Localization/Monoidal.lean#L101
@CategoryTheory.Localization.Monoidal.tensorBifunctorIso definition missing documentation string
|
|
lint mathlib:
Mathlib/CategoryTheory/Localization/Monoidal.lean#L115
@CategoryTheory.Localization.Monoidal.leftUnitor definition missing documentation string
|
|
lint mathlib:
Mathlib/CategoryTheory/Localization/Monoidal.lean#L121
@CategoryTheory.Localization.Monoidal.rightUnitor definition missing documentation string
|
|
lint mathlib:
Mathlib/CategoryTheory/Localization/Monoidal.lean#L127
@CategoryTheory.Localization.Monoidal.associator definition missing documentation string
|
|
build mathlib
The process '/usr/bin/bash' failed with exit code 1
|
Loading