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:
Riccardo Brasca riccardobrasca
riccardobrasca
/ mathlib_useless.txt
Created
September 16, 2022 15:36
This file has been truncated, but you can view the full file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |
riccardobrasca
/ removable.txt
Last active
September 14, 2022 12:30
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |
riccardobrasca
/ useless_number.txt
Last active
September 14, 2022 12:29
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |
riccardobrasca
/ full_not_challenge_no_namespace.txt
Created
September 14, 2022 11:21
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |
riccardobrasca
/ full_not_challenge.txt
Created
September 14, 2022 10:57
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |
riccardobrasca
/ keybase.md
Created
April 23, 2020 14:57