I hereby claim:
- I am riccardobrasca on github.
- I am riccardobrasca (https://keybase.io/riccardobrasca) on keybase.
- I have a public key ASACnbWPXBFZXPOSF45ACdVSl2uyCSGr5ymYpFq4WmFkqgo
To claim this, I am signing this object:
abelianization_congr_of | |
abelianization_congr_refl | |
abelianization_congr_symm | |
abelianization_congr_trans | |
abelianization.equiv_of_comm | |
abelianization.equiv_of_comm_apply | |
abelianization.equiv_of_comm_symm_apply | |
abelianization.fintype | |
abelianization.hom_ext | |
abelianization.inhabited |
AddCommGroup.add_subgroup.equiv_top_symm_apply | |
AddCommGroup.colimit_comparison | |
AddCommGroup.hom_product_comparison | |
add_comm_group.limit_on_nat_torsion_free | |
AddCommGroup.tensor_uncurry_curry | |
AddCommGroup.zmod_resolution_is_resolution | |
AddCommGroup.zmod_resolution_pi | |
add_equiv.mk_symm_apply | |
add_equiv.ulift_symm_apply | |
add_monoid_hom.comp_mem_filtration |
AddCommGroup.add_subgroup.equiv_top_symm_apply 1 | |
AddCommGroup.colimit_comparison 1 | |
AddCommGroup.hom_product_comparison 1 | |
AddCommGroup.is_iso_hom_product_comparison 1 | |
add_comm_group.limit_on_nat_torsion_free 1 | |
AddCommGroup.tensor_functor_flip_additive 1 | |
AddCommGroup.tensor_uncurry_curry 1 | |
AddCommGroup.zmod_resolution_is_resolution 1 | |
AddCommGroup.zmod_resolution_pi 1 | |
add_equiv.mk_symm_apply 1 |
limit_cone'_cone | |
limit_cone'_is_limit | |
ulift_obj | |
has_colimits_of_size | |
equiv_top | |
equiv_top_apply_coe | |
equiv_top_symm_apply | |
coe_of' | |
colimit_comparison | |
direct_sum_bicone |
Ab.limit_cone'_cone | |
Ab.limit_cone'_is_limit | |
Ab.ulift_obj | |
AddCommGroup.Ab.category_theory.limits.has_colimits_of_size | |
AddCommGroup.add_subgroup.equiv_top | |
AddCommGroup.add_subgroup.equiv_top_apply_coe | |
AddCommGroup.add_subgroup.equiv_top_symm_apply | |
AddCommGroup.coe_of' | |
AddCommGroup.colimit_comparison | |
AddCommGroup.direct_sum_bicone |
I hereby claim:
To claim this, I am signing this object: