Description: The mapping G between fundamental groups is a group homomorphism. (Contributed by Mario Carneiro, 10-Aug-2015) (Revised by Mario Carneiro, 23-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pi1co.p | |
|
pi1co.q | |
||
pi1co.v | |
||
pi1co.g | |
||
pi1co.j | |
||
pi1co.f | |
||
pi1co.a | |
||
pi1co.b | |
||
Assertion | pi1coghm | |