more on commutator subgroups #3365
Annotations
2 errors
|
Run coq-community/docker-coq-action@v1:
theories/Algebra/Groups/Subgroup.v#L228
Expected a single focused goal but 6 goals are focused.
Command exited with non-zero status 1
|
|
Run coq-community/docker-coq-action@v1:
theories/Algebra/Groups/GrpPullback.v#L90
In environment
A, B, C : Group
f : B $-> A
g : C $-> A
The term "Build_Group (Pullback f g) ?op ?unit ?inv ?Associative0" has type
"LeftIdentity ?op ?unit ->
RightIdentity ?op ?unit ->
LeftInverse ?op ?inv ?unit ->
RightInverse ?op ?inv ?unit ->
(forall z y x : Pullback f g, x * y * z = x * (y * z)) -> Group"
while it is expected to have type "Group".
Command exited with non-zero status 1
|
Loading