diff --git a/algebra/quotient_group.hlean b/algebra/quotient_group.hlean index c2e0b2b..963cd70 100644 --- a/algebra/quotient_group.hlean +++ b/algebra/quotient_group.hlean @@ -247,6 +247,7 @@ namespace group ------------------------------------------------ -- FIRST ISOMORPHISM THEOREM +------------------------------------------------ definition kernel_quotient_extension {A B : AbGroup} (f : A →g B) : quotient_ab_group (kernel_subgroup f) →g B := @@ -371,7 +372,8 @@ definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B) exact is_embedding_kernel_quotient_extension f end -definition ab_group_first_iso_thm (A B : AbGroup) (f : A →g B) : quotient_ab_group (kernel_subgroup f) ≃g ab_image f := +definition ab_group_first_iso_thm (A B : AbGroup) (f : A →g B) + : quotient_ab_group (kernel_subgroup f) ≃g ab_image f := begin fapply isomorphism.mk, exact ab_group_kernel_quotient_to_image f,