From c09f5689923cee4804e12bbe8e552dc53953dfb0 Mon Sep 17 00:00:00 2001 From: Steve Awodey Date: Thu, 26 Jan 2017 14:58:19 -0500 Subject: [PATCH] trivial --- algebra/quotient_group.hlean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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,