Theoremshom_add, hom_nsmul, hom_zero, fst_hom, hom_add, hom_zero, instIsCommAddMonObj, lift_hom, snd_hom, uniqueHomToTrivial_default_hom, add_comp, add_comp_assoc, add_eq_add, comp_add, comp_add_assoc, comp_nsmul, comp_nsmul_assoc, comp_zero, comp_zero_assoc, instIsAddMonHomAddOfIsCommAddMonObj, instIsAddMonHomFst, instIsAddMonHomLift, instIsAddMonHomSnd, instIsAddMonHomToAddUnit, instIsAddMonHomZero, lift_comp_zero_left, lift_comp_zero_left_assoc, lift_comp_zero_right, lift_comp_zero_right_assoc, lift_lift_assoc, nsmul_comp, nsmul_comp_assoc, ofRepresentableBy_add, ofRepresentableBy_yonedaAddMonObjRepresentableBy, ofRepresentableBy_zero, zero_comp, zero_comp_assoc, zero_eq_zero, homAddEquiv_apply, homAddEquiv_symm_apply, homMulEquiv_apply, homMulEquiv_symm_apply, homAddMonoidHom_apply, homMonoidHom_apply, map_add', map_mul, map_one, map_zero', addEquivCongrRight_apply, addEquivCongrRight_symm_apply, add_def, mulEquivCongrRight_apply, mulEquivCongrRight_symm_apply, mul_def, one_def, zero_def, hom_mul, hom_one, hom_pow, fst_hom, hom_mul, hom_one, instIsCommMonObj, lift_hom, snd_hom, uniqueHomToTrivial_default_hom, comp_mul, comp_mul_assoc, comp_one, comp_one_assoc, comp_pow, comp_pow_assoc, instIsMonHomFst, instIsMonHomLift, instIsMonHomMulOfIsCommMonObj, instIsMonHomOne, instIsMonHomSnd, instIsMonHomToUnit, lift_comp_one_left, lift_comp_one_left_assoc, lift_comp_one_right, lift_comp_one_right_assoc, lift_lift_assoc, mul_comp, mul_comp_assoc, mul_eq_mul, ofRepresentableBy_mul, ofRepresentableBy_one, ofRepresentableBy_yonedaMonObjRepresentableBy, one_comp, one_comp_assoc, one_eq_one, pow_comp, pow_comp_assoc, essImage_yonedaAddMon, essImage_yonedaMon, instFaithfulMonFunctorOppositeMonCatYonedaMon, instFaithfulMonFunctorOppositeMonCatyonedaAddMon, instFullMonFunctorOppositeMonCatYonedaMon, instFullMonFunctorOppositeMonCatyonedaAddMon, instHasZeroObjectAddMon, instHasZeroObjectMon, isCommAddMonObj_iff_isAddCommutative, isCommMonObj_iff_isMulCommutative, yonedaAddMonObjIsoOfRepresentableBy_hom_app_hom_apply, yonedaAddMonObjIsoOfRepresentableBy_inv_app_hom_apply, yonedaAddMonObj_map, yonedaAddMonObj_obj_coe, yonedaAddMon_map_app, yonedaAddMon_naturality, yonedaAddMon_naturality_assoc, yonedaAddMon_obj, yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply, yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply, yonedaMonObj_map, yonedaMonObj_obj_coe, yonedaMon_map_app, yonedaMon_naturality, yonedaMon_naturality_assoc, yonedaMon_obj | 120 |