From 704717e9ae53b92da20e57bd8e50c2f8a2400ee7 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 3 Nov 2016 15:34:06 -0400
Subject: [PATCH] minor changes

---
 .gitignore             |   1 +
 TAGS                   | 692 -----------------------------------------
 algebra/subgroup.hlean |  11 +-
 homotopy/smash.hlean   |  36 ++-
 move_to_lib.hlean      |  17 +-
 5 files changed, 57 insertions(+), 700 deletions(-)
 delete mode 100644 TAGS

diff --git a/.gitignore b/.gitignore
index 0c8c123..3a19649 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,6 +13,7 @@ GPATH
 GRTAGS
 GSYMS
 GTAGS
+TAGS
 Makefile
 *.cmake
 CMakeFiles/
diff --git a/TAGS b/TAGS
deleted file mode 100644
index f016d47..0000000
--- a/TAGS
+++ /dev/null
@@ -1,692 +0,0 @@
-
-homotopy/spherical_fibrations.hlean,1152
-  definition pointed_BFspherical_fibrations.pointed_BF
50,1310
-  definition pBGspherical_fibrations.pBG
15,414
-  definition BF_of_BG_mulspherical_fibrations.BF_of_BG_mul
95,2692
-  definition BFspherical_fibrations.BF
47,1244
-    definition thom_spacespherical_fibrations.thom.thom_space
109,3059
-  definition mirrorspherical_fibrations.mirror
23,605
-  definition Gspherical_fibrations.G
17,484
-  definition G_charspherical_fibrations.G_char
20,537
-  definition BG_mulspherical_fibrations.BG_mul
78,2096
-  definition BF_succspherical_fibrations.BF_succ
55,1496
-  definition BG_of_BFspherical_fibrations.BG_of_BF
71,1919
-  definition BF_of_BGspherical_fibrations.BF_of_BG
62,1681
-    protected definition secspherical_fibrations.thom.sec
104,2964
-    definition tauspherical_fibrations.two_sphere.tau
144,4263
-  definition BG_succspherical_fibrations.BG_succ
39,1009
-  definition pBFspherical_fibrations.pBF
53,1426
-  definition pointed_BGspherical_fibrations.pointed_BG
12,301
-  definition BF_mulspherical_fibrations.BF_mul
87,2401
-  definition BGspherical_fibrations.BG
9,233
-  definition S_of_BGspherical_fibrations.S_of_BG
36,936
-
-homotopy/homotopy_groups.hlean,743
-    definition group_equiv_onemy.group_equiv_one
44,1189
-    theorem group_equiv_mul_assocmy.group_equiv_mul_assoc
52,1423
-    theorem group_equiv_mul_onemy.group_equiv_mul_one
58,1710
-    definition group_equiv_invmy.group_equiv_inv
46,1234
-  theorem ap1_conmy.ap1_con
25,626
-    theorem group_equiv_mul_left_invmy.group_equiv_mul_left_inv
61,1852
-    definition group_equiv_closedmy.group_equiv_closed
65,2030
-    theorem group_equiv_one_mulmy.group_equiv_one_mul
55,1568
-    definition group_equiv_mulmy.group_equiv_mul
42,1118
-  definition apn_composemy.apn_compose
18,411
-  definition apn_conmy.apn_con
30,784
-  definition homotopy_group_homomorphismeq.homotopy_group_homomorphism
83,2503
-  definition tr_mulmy.tr_mul
34,931
-
-homotopy/sample.hlean,1236
-    definition is_conn_of_map_from_unithomotopy.is_conn_of_map_from_unit
97,3227
-  definition is_connhomotopy.is_conn
12,308
-    definition elimhomotopy.is_conn_fun.elim
51,1665
-  definition is_conn_homotopyhomotopy.is_conn_homotopy
154,4935
-    definition introhomotopy.is_conn_fun.intro
70,2280
-  definition is_conn_funhomotopy.is_conn_fun
24,636
-    definition rechomotopy.is_conn_fun.rec
39,1224
-    definition is_conn_of_map_to_unithomotopy.is_conn_of_map_to_unit
88,2969
-  definition merely_of_minus_one_connhomotopy.merely_of_minus_one_conn
131,4268
-  definition minus_one_conn_of_merelyhomotopy.minus_one_conn_of_merely
134,4364
-  definition is_conn_susphomotopy.is_conn_susp
165,5320
-  definition minus_one_conn_of_surjectivehomotopy.minus_one_conn_of_surjective
117,3839
-    definition is_conn_fun_from_unithomotopy.is_conn_fun_from_unit
106,3534
-  definition is_surjection_of_minus_one_connhomotopy.is_surjection_of_minus_one_conn
124,4078
-  definition is_conn_equiv_closedhomotopy.is_conn_equiv_closed
15,404
-  definition minus_two_connhomotopy.minus_two_conn
159,5215
-    definition elim_βhomotopy.is_conn_fun.elim_β
54,1767
-    definition retract_of_conn_is_connhomotopy.retract_of_conn_is_conn
143,4572
-
-homotopy/LES_applications.hlean,701
-    definition add_plus_one_minus_oneis_conn.add_plus_one_minus_one
110,4328
-    definition add_plus_one_succis_conn.add_plus_one_succ
111,4398
-  definition eq_even_or_eq_oddnat.eq_even_or_eq_odd
7,278
-  definition join_empty_rightis_conn.join_empty_right
87,3633
-    definition succ_add_plus_oneis_conn.succ_add_plus_one
114,4613
-  definition rec_on_even_oddnat.rec_on_even_odd
16,554
-  theorem is_surjective_π_of_is_connectedis_conn.is_surjective_π_of_is_connected
69,2838
-    definition minus_one_add_plus_oneis_conn.minus_one_add_plus_one
112,4480
-  definition natural_square2is_conn.natural_square2
102,4049
-  theorem is_equiv_π_of_is_connectedis_conn.is_equiv_π_of_is_connected
32,921
-
-homotopy/LES_of_homotopy_groups.hlean,8241
-  definition LES_of_homotopy_groups3_1chain_complex.LES_of_homotopy_groups3_1
882,34115
-  definition is_exact_LES_of_homotopy_groups3chain_complex.is_exact_LES_of_homotopy_groups3
857,32991
-  definition LES_of_homotopy_groups3_4chain_complex.LES_of_homotopy_groups3_4
888,34446
-  definition homotopy_groups_fun2chain_complex.homotopy_groups_fun2
544,20051
-  definition LES_of_homotopy_groups_mul3add2'chain_complex.LES_of_homotopy_groups_mul3add2'
477,17839
-  definition LES_of_homotopy_groups3_3chain_complex.LES_of_homotopy_groups3_3
886,34336
-  definition tr_mul_trchain_complex.tr_mul_tr
500,18472
-  definition is_exact_fiber_sequencechain_complex.is_exact_fiber_sequence
80,2506
-  definition boundary_mapchain_complex.boundary_map
225,8385
-  theorem fiber_sequence_fun_phomotopychain_complex.fiber_sequence_fun_phomotopy
216,8057
-  definition is_exact_LES_of_homotopy_groupschain_complex.is_exact_LES_of_homotopy_groups
410,15146
-  definition LES_of_homotopy_groups3_2chain_complex.LES_of_homotopy_groups3_2
884,34221
-  definition homotopy_groups_mul3add2chain_complex.homotopy_groups_mul3add2
254,9279
-  definition type_LES_of_homotopy_groupschain_complex.type_LES_of_homotopy_groups
386,14323
-  definition homotopy_groups_fun2_add1_5chain_complex.homotopy_groups_fun2_add1_5
592,22238
-  definition homotopy_groups_fun'chain_complex.homotopy_groups_fun'
276,10198
-  definition fin_prod_nat_equiv_natchain_complex.fin_prod_nat_equiv_nat
620,23461
-  definition fiber_sequence_helpernchain_complex.fiber_sequence_helpern
54,1759
-  theorem fiber_sequence_carrier_pequiv_eq_point_eq_idpchain_complex.fiber_sequence_carrier_pequiv_eq_point_eq_idp
177,6559
-  definition homotopy_groups_funchain_complex.homotopy_groups_fun
260,9523
-  definition fiber_sequence_carrierchain_complex.fiber_sequence_carrier
62,1987
-  definition homotopy_groups_fun_add3chain_complex.homotopy_groups_fun_add3
312,11532
-  definition comm_group_LES_of_homotopy_groupschain_complex.comm_group_LES_of_homotopy_groups
486,18179
-  definition LES_of_homotopy_groups2chain_complex.LES_of_homotopy_groups2
779,30007
-  definition LES_of_homotopy_groups_mul3add1chain_complex.LES_of_homotopy_groups_mul3add1
451,17024
-  definition homotopy_groups_add3chain_complex.homotopy_groups_add3
240,8787
-  definition LES_of_homotopy_groups3_0chain_complex.LES_of_homotopy_groups3_0
880,34009
-  definition homotopy_groups3eq2chain_complex.homotopy_groups3eq2
794,30462
-  definition fiber_sequence_helperchain_complex.fiber_sequence_helper
50,1612
-  definition homotopy_groups2_pequiv'chain_complex.homotopy_groups2_pequiv'
641,24217
-  definition fiber_sequence_carrier_equiv_inv_eqchain_complex.fiber_sequence_carrier_equiv_inv_eq
125,4437
-  definition homotopy_groups2chain_complex.homotopy_groups2
526,19349
-  definition fiber_sequence_pequiv_homotopy_groupschain_complex.fiber_sequence_pequiv_homotopy_groups
319,11794
-  definition is_homomorphism_cast_loop_space_succ_eq_inchain_complex.is_homomorphism_cast_loop_space_succ_eq_in
504,18597
-  definition fiber_sequence_funchain_complex.fiber_sequence_fun
65,2078
-  definition LES_of_homotopy_groups_mul3add1'chain_complex.LES_of_homotopy_groups_mul3add1'
471,17652
-  definition nat_of_str_6Schain_complex.nat_of_str_6S
610,23009
-  definition homotopy_groups_mul3chain_complex.homotopy_groups_mul3
244,8912
-  definition LES_of_homotopy_groupschain_complex.LES_of_homotopy_groups
401,14827
-  definition homotopy_groups_fun2_add1_4chain_complex.homotopy_groups_fun2_add1_4
583,21862
-  definition homotopy_groups3chain_complex.homotopy_groups3
786,30178
-  definition fiber_sequence_pequiv_homotopy_groups_3_phomotopychain_complex.fiber_sequence_pequiv_homotopy_groups_3_phomotopy
336,12382
-  definition homotopy_groupschain_complex.homotopy_groups
234,8658
-  definition homotopy_groups_fun2_add1_2chain_complex.homotopy_groups_fun2_add1_2
565,21099
-  definition homotopy_groups_fun2_phomotopychain_complex.homotopy_groups_fun2_phomotopy
689,26060
-  definition LES_of_homotopy_groups3_5chain_complex.LES_of_homotopy_groups3_5
890,34556
-  definition LES_of_homotopy_groups_fun3_1chain_complex.LES_of_homotopy_groups_fun3_1
899,34906
-  definition group_LES_of_homotopy_groups3_0chain_complex.group_LES_of_homotopy_groups3_0
916,35755
-  definition CommGroup_LES_of_homotopy_groups3chain_complex.CommGroup_LES_of_homotopy_groups3
933,36775
-  definition is_exact_type_LES_of_homotopy_groups2chain_complex.is_exact_type_LES_of_homotopy_groups2
772,29801
-  theorem homotopy_groups_fun_eqchain_complex.homotopy_groups_fun_eq
287,10605
-  definition LES_of_homotopy_groups_mul3'chain_complex.LES_of_homotopy_groups_mul3'
465,17477
-  definition LES_of_homotopy_groups_fun3_0chain_complex.LES_of_homotopy_groups_fun3_0
896,34780
-  definition comm_group_LES_of_homotopy_groups3chain_complex.comm_group_LES_of_homotopy_groups3
923,36148
-  definition homotopy_groups_fun2_add1_1chain_complex.homotopy_groups_fun2_add1_1
560,20890
-  definition fiber_sequence_pequiv_homotopy_groups_add3chain_complex.fiber_sequence_pequiv_homotopy_groups_add3
331,12158
-  definition homotopy_groups_fun'_add3chain_complex.homotopy_groups_fun'_add3
283,10455
-  definition is_homomorphism_inversechain_complex.is_homomorphism_inverse
514,19037
-  theorem fiber_sequence_fun_phomotopy_helperchain_complex.fiber_sequence_fun_phomotopy_helper
194,7170
-  definition homotopy_groups_fun_add6chain_complex.homotopy_groups_fun_add6
270,9919
-  definition LES_of_homotopy_groups_fun3_5chain_complex.LES_of_homotopy_groups_fun3_5
911,35532
-  theorem fiber_sequence_phomotopy_homotopy_groups'chain_complex.fiber_sequence_phomotopy_homotopy_groups'
344,12670
-  definition LES_of_homotopy_groups_fun3_4chain_complex.LES_of_homotopy_groups_fun3_4
908,35381
-  definition is_exact_type_LES_of_homotopy_groupschain_complex.is_exact_type_LES_of_homotopy_groups
393,14582
-  definition fiber_sequence_carrier_equiv_eqchain_complex.fiber_sequence_carrier_equiv_eq
110,3830
-  definition LES_of_homotopy_groups_mul3chain_complex.LES_of_homotopy_groups_mul3
444,16814
-  definition LES_of_homotopy_groups3chain_complex.LES_of_homotopy_groups3
850,32786
-  theorem fiber_sequence_phomotopy_homotopy_groupschain_complex.fiber_sequence_phomotopy_homotopy_groups
377,13934
-  definition LES_of_homotopy_groups_mul3add2chain_complex.LES_of_homotopy_groups_mul3add2
458,17246
-  definition homotopy_groups_fun3chain_complex.homotopy_groups_fun3
804,30894
-  definition homotopy_groups_mul3add1chain_complex.homotopy_groups_mul3add1
249,9089
-  definition fiber_sequence_carrier_pequiv_inv_eqchain_complex.fiber_sequence_carrier_pequiv_inv_eq
149,5360
-  definition fiber_sequence_carrier_pequivchain_complex.fiber_sequence_carrier_pequiv
134,4778
-  theorem fiber_sequence_fun_eqchain_complex.fiber_sequence_fun_eq
208,7685
-  definition fiber_sequence_carrier_equivchain_complex.fiber_sequence_carrier_equiv
84,2664
-  definition nat_of_strchain_complex.nat_of_str
604,22800
-  definition fiber_sequencechain_complex.fiber_sequence
70,2251
-  definition str_of_natchain_complex.str_of_nat
607,22917
-  definition homomorphism_LES_of_homotopy_groups_fun3chain_complex.homomorphism_LES_of_homotopy_groups_fun3
937,36984
-  definition homotopy_groups_fun3eq2chain_complex.homotopy_groups_fun3eq2
816,31572
-  definition homotopy_groups_fun2_add1_0chain_complex.homotopy_groups_fun2_add1_0
555,20681
-  definition fiber_sequence_fun_eq_helperchain_complex.fiber_sequence_fun_eq_helper
157,5693
-  definition homotopy_groups2_add1chain_complex.homotopy_groups2_add1
534,19628
-  definition homotopy_groups_fun2_add1_3chain_complex.homotopy_groups_fun2_add1_3
574,21486
-  definition LES_of_homotopy_groups_fun3_3chain_complex.LES_of_homotopy_groups_fun3_3
905,35239
-  definition LES_of_homotopy_groups_fun3_2chain_complex.LES_of_homotopy_groups_fun3_2
902,35041
-  definition type_LES_of_homotopy_groups2chain_complex.type_LES_of_homotopy_groups2
758,29331
-  definition homotopy_groups2_pequivchain_complex.homotopy_groups2_pequiv
684,25855
-  definition group_LES_of_homotopy_groupschain_complex.group_LES_of_homotopy_groups
483,18035
-  definition fiber_sequence_carrier_pequiv_eqchain_complex.fiber_sequence_carrier_pequiv_eq
142,5004
-
-group_theory/constructions.hlean,10223
-  definition normal_subgroup_kernelgroup.normal_subgroup_kernel
721,26462
-  structure Rinvgroup.normal_subgroup_rel.Rinv
23,565
-    | rinvgroup.generating_relation'.rinv
614,22880
-  | rreflgroup.free_comm_group.fcg_rel.rrefl
435,16260
-  definition fcg_mulgroup.free_comm_group.fcg_mul
492,18417
-  theorem subgroup_one_mulgroup.subgroup_one_mul
82,3290
-  structure rec_ongroup.normal_subgroup_rel.rec_on
23,565
-    definition quotient_comm_group_gengroup.quotient_comm_group_gen
633,23558
-  structure Rgroup.subgroup_rel.R
17,410
-  theorem kernel_mulgroup.kernel_mul
680,25173
-  definition sggroup.sg
65,2698
-  theorem subgroup_mul_assocgroup.subgroup_mul_assoc
79,3183
-    | rmulgroup.generating_relation'.rmul
613,22779
-  definition subgroup_onegroup.subgroup_one
68,2786
-  definition is_reflexive_Rgroup.free_group.is_reflexive_R
290,10899
-  inductive cases_ongroup.free_group.free_group_rel.cases_on
274,10175
-  abbreviation subgroup_has_onegroup.subgroup_has_one
28,791
-  definition free_group_onegroup.free_group.free_group_one
315,11815
-  theorem quotient_rel_symmgroup.quotient_rel_symm
120,4459
-  | resp_appendgroup.free_group.free_group_rel.resp_append
278,10373
-  definition fcg_carriergroup.free_comm_group.fcg_carrier
449,16786
-  definition group_qggroup.group_qg
210,7984
-  theorem product_one_mulgroup.product_one_mul
240,9105
-  definition free_group_inclusiongroup.free_group_inclusion
376,13925
-  structure destructgroup.subgroup_rel.destruct
17,410
-  definition free_comm_group_inclusiongroup.free_comm_group_inclusion
560,20652
-  theorem free_group_mul_left_invgroup.free_group.free_group_mul_left_inv
348,12968
-  definition group_prodgroup.group_prod
255,9511
-  | rtransgroup.free_group.free_group_rel.rtrans
280,10519
-  definition free_comm_group_homgroup.free_comm_group_hom
575,21250
-    definition normal_generating_relationgroup.normal_generating_relation
625,23357
-  definition free_comm_groupgroup.free_comm_group
555,20471
-  structure to_subgroup_relgroup.normal_subgroup_rel.to_subgroup_rel
23,565
-  definition free_group_invgroup.free_group.free_group_inv
316,11879
-  structure Rmulgroup.normal_subgroup_rel.Rmul
23,565
-  theorem rel_respect_reversegroup.free_comm_group.rel_respect_reverse
468,17493
-  theorem free_group_mul_assocgroup.free_group.free_group_mul_assoc
327,12349
-  structure normal_subgroup_relgroup.normal_subgroup_rel
23,565
-    definition gr_mulgroup.gr_mul
622,23272
-  theorem product_mul_assocgroup.product_mul_assoc
237,8989
-  definition quotient_comm_groupgroup.quotient_comm_group
221,8428
-  theorem fcg_one_mulgroup.free_comm_group.fcg_one_mul
509,18950
-  abbreviation subgroup_respect_mulgroup.subgroup_respect_mul
29,860
-  definition comm_group_prodgroup.comm_group_prod
262,9779
-  inductive fcg_relgroup.free_comm_group.fcg_rel.rec
434,16208
-  definition quotient_relgroup.quotient_rel
115,4268
-    inductive dirsum_relgroup.dirsum_rel
643,23866
-  theorem quotient_mul_assocgroup.quotient_mul_assoc
172,6919
-  theorem product_mul_commgroup.product_mul_comm
249,9371
-  definition subgroupgroup.subgroup
102,3873
-  theorem fgh_helper_respect_comm_relgroup.fgh_helper_respect_comm_rel
563,20753
-  theorem quotient_rel_transgroup.quotient_rel_trans
123,4623
-  definition kernelgroup.kernel
678,25082
-  definition qggroup.qg
157,6375
-  definition comm_subgroupgroup.comm_subgroup
109,4111
-    definition direct_sumgroup.direct_sum
646,23998
-  structure normal_subgroup_relgroup.normal_subgroup_rel.rec
23,565
-    definition gr_invgroup.gr_inv
620,23198
-  theorem rel_cons_concatgroup.free_comm_group.rel_cons_concat
479,17905
-  theorem fgh_helper_mulgroup.fgh_helper_mul
393,14566
-  definition comm_group_sggroup.comm_group_sg
105,3947
-  | resp_appendgroup.free_comm_group.fcg_rel.resp_append
439,16420
-  definition fn_of_free_group_homgroup.fn_of_free_group_hom
413,15391
-  theorem fcg_mul_assocgroup.free_comm_group.fcg_mul_assoc
500,18669
-  theorem product_mul_left_invgroup.product_mul_left_inv
246,9271
-  definition comm_group_qggroup.comm_group_qg
217,8257
-  definition normal_subgroup_rel_commgroup.normal_subgroup_rel_comm
39,1314
-  | cancel1group.free_comm_group.fcg_rel.cancel1
436,16290
-  definition fgh_helpergroup.fgh_helper
379,14019
-  definition product_onegroup.product_one
226,8642
-    mkgroup.normal_subgroup_rel.mk
24,627
-    definition generating_relationgroup.generating_relation
617,23026
-  | cancel2group.free_group.free_group_rel.cancel2
277,10322
-    | rmkgroup.dirsum_rel.rmk
644,23910
-  structure no_confusiongroup.subgroup_rel.no_confusion
17,410
-  inductive rec_ongroup.free_comm_group.fcg_rel.rec_on
434,16208
-  theorem is_normal_subgroup_kernelgroup.is_normal_subgroup_kernel
707,25917
-  theorem fgh_helper_respect_relgroup.fgh_helper_respect_rel
382,14131
-  abbreviation is_normal_subgroupgroup.is_normal_subgroup
31,998
-    | rinclgroup.generating_relation'.rincl
612,22730
-  definition free_group_carriergroup.free_group.free_group_carrier
287,10767
-  theorem quotient_mul_onegroup.quotient_mul_one
187,7357
-  | rtransgroup.free_comm_group.fcg_rel.rtrans
441,16545
-  structure Rinvgroup.subgroup_rel.Rinv
17,410
-  definition fn_of_free_comm_group_homgroup.fn_of_free_comm_group_hom
586,21759
-    mkgroup.subgroup_rel.mk
18,442
-    definition gr_onegroup.gr_one
619,23155
-  theorem is_normal_subgroup_rev'group.is_normal_subgroup_rev'
52,1969
-  structure subgroup_relgroup.subgroup_rel.rec
17,410
-  structure Rgroup.normal_subgroup_rel.R
23,565
-  inductive fcg_relgroup.free_comm_group.fcg_rel
434,16208
-  definition quotient_onegroup.quotient_one
161,6480
-  theorem quotient_rel_reflgroup.quotient_rel_refl
118,4339
-  theorem product_mul_onegroup.product_mul_one
243,9188
-  definition free_comm_group_hom_equiv_fngroup.free_comm_group_hom_equiv_fn
590,21903
-  definition subgroup_kernelgroup.subgroup_kernel
699,25721
-  | cancel1group.free_group.free_group_rel.cancel1
276,10271
-  definition product_mulgroup.product_mul
229,8782
-  theorem quotient_rel_resp_mulgroup.quotient_rel_resp_mul
140,5543
-  definition free_groupgroup.free_group
371,13774
-  theorem is_normal_subgroup'group.is_normal_subgroup'
36,1200
-  definition productgroup.product
259,9701
-  definition free_group_homgroup.free_group_hom
402,14897
-  theorem normal_subgroup_insertgroup.normal_subgroup_insert
55,2094
-  theorem quotient_mul_left_invgroup.quotient_mul_left_inv
193,7512
-  structure Rmulgroup.subgroup_rel.Rmul
17,410
-  theorem quotient_rel_resp_invgroup.quotient_rel_resp_inv
131,5061
-  theorem fcg_mul_commgroup.free_comm_group.fcg_mul_comm
536,19740
-  definition group_free_comm_groupgroup.group_free_comm_group
551,20268
-    inductive cases_ongroup.dirsum_rel.cases_on
643,23866
-  structure Ronegroup.normal_subgroup_rel.Rone
23,565
-  structure is_normalgroup.normal_subgroup_rel.is_normal
23,565
-  abbreviation subgroup_to_relgroup.subgroup_to_rel
27,725
-  definition is_reflexive_Rgroup.free_comm_group.is_reflexive_R
452,16904
-  structure cases_ongroup.normal_subgroup_rel.cases_on
23,565
-  | rflipgroup.free_comm_group.fcg_rel.rflip
438,16378
-  definition product_invgroup.product_inv
227,8704
-  structure Ronegroup.subgroup_rel.Rone
17,410
-  | cancel2group.free_comm_group.fcg_rel.cancel2
437,16334
-  inductive free_group_relgroup.free_group.free_group_rel
274,10175
-  definition group_sggroup.group_sg
98,3680
-  definition subgroup_invgroup.subgroup_inv
69,2861
-  theorem rel_respect_reversegroup.free_group.rel_respect_reverse
305,11444
-    inductive dirsum_relgroup.dirsum_rel.rec
643,23866
-  definition quotient_groupgroup.quotient_group
214,8177
-  definition free_group_mulgroup.free_group.free_group_mul
319,12069
-    definition dirsum_carriergroup.dirsum_carrier
641,23724
-    inductive rec_ongroup.generating_relation'.rec_on
611,22688
-  structure destructgroup.normal_subgroup_rel.destruct
23,565
-    inductive generating_relation'group.generating_relation'
611,22688
-  theorem quotient_mul_commgroup.quotient_mul_comm
199,7679
-  theorem kernel_invgroup.kernel_inv
690,25493
-  inductive rec_ongroup.free_group.free_group_rel.rec_on
274,10175
-  theorem free_group_one_mulgroup.free_group.free_group_one_mul
336,12637
-  theorem rel_respect_flipgroup.free_comm_group.rel_respect_flip
457,17078
-  inductive free_group_relgroup.free_group.free_group_rel.rec
274,10175
-    inductive cases_ongroup.generating_relation'.cases_on
611,22688
-  definition fcg_invgroup.free_comm_group.fcg_inv
489,18234
-  theorem subgroup_mul_commgroup.subgroup_mul_comm
91,3530
-    inductive rec_ongroup.dirsum_rel.rec_on
643,23866
-  definition fcg_onegroup.free_comm_group.fcg_one
488,18177
-  structure rec_ongroup.subgroup_rel.rec_on
17,410
-  theorem subgroup_mul_left_invgroup.subgroup_mul_left_inv
88,3442
-  theorem fcg_mul_left_invgroup.free_comm_group.fcg_mul_left_inv
521,19267
-  theorem rel_respect_flipgroup.free_group.rel_respect_flip
295,11073
-  | rreflgroup.free_group.free_group_rel.rrefl
275,10234
-    inductive generating_relation'group.generating_relation'.rec
611,22688
-  theorem quotient_one_mulgroup.quotient_one_mul
181,7202
-  definition quotient_invgroup.quotient_inv
162,6543
-  theorem is_equivalence_quotient_relgroup.is_equivalence_quotient_rel
150,6091
-  theorem free_group_mul_onegroup.free_group.free_group_mul_one
342,12802
-  theorem is_normal_subgroup_revgroup.is_normal_subgroup_rev
45,1563
-  structure no_confusiongroup.normal_subgroup_rel.no_confusion
23,565
-  structure subgroup_relgroup.subgroup_rel
17,410
-  definition group_free_groupgroup.group_free_group
367,13543
-    | ronegroup.generating_relation'.rone
615,22950
-  theorem fcg_mul_onegroup.free_comm_group.fcg_mul_one
515,19108
-  abbreviation subgroup_respect_invgroup.subgroup_respect_inv
30,929
-  definition free_group_hom_equiv_fngroup.free_group_hom_equiv_fn
417,15520
-  inductive cases_ongroup.free_comm_group.fcg_rel.cases_on
434,16208
-  theorem subgroup_mul_onegroup.subgroup_mul_one
85,3366
-  definition comm_productgroup.comm_product
265,9929
-  definition subgroup_mulgroup.subgroup_mul
71,2957
-  structure cases_ongroup.subgroup_rel.cases_on
17,410
-  definition quotient_mulgroup.quotient_mul
164,6665
-
-homotopy/fin.hlean,557
-  definition my_succfin.my_succ
30,720
-inductive is_succis_succ.rec
13,236
-  definition has_one_finfin.has_one_fin
46,1254
-  protected definition addfin.add
40,1035
-  definition has_add_finfin.has_add_fin
49,1401
-definition is_succ_bit0is_succ_bit0
24,585
-inductive rec_onis_succ.rec_on
13,236
-inductive is_succis_succ
13,236
-| mkis_succ.mk
14,268
-definition is_succ_add_rightis_succ_add_right
18,339
-inductive cases_onis_succ.cases_on
13,236
-  definition has_zero_finfin.has_zero_fin
43,1114
-definition is_succ_add_leftis_succ_add_left
21,460
-
-group_theory/basic.hlean,2779
-  definition to_respect_mulgroup.to_respect_mul
94,3090
-  definition structgroup.homomorphism.struct
88,2858
-    mkgroup.homomorphism.mk
82,2703
-  definition comm_group_Group_of_CommGroupgroup.comm_group_Group_of_CommGroup
30,953
-  definition is_homomorphism_idgroup.is_homomorphism_id
76,2559
-  theorem to_respect_invgroup.to_respect_inv
100,3245
-  definition to_ginvgroup.to_ginv
151,5068
-  definition Set_of_Groupgroup.Set_of_Group
25,788
-  theorem respect_onegroup.respect_one
51,1730
-  definition pointed_Groupgroup.pointed_Group
23,631
-  definition precategory_groupgroup.precategory_group
183,6085
-  definition Group_of_CommGroupgroup.Group_of_CommGroup
27,853
-  structure destructgroup.homomorphism.destruct
81,2660
-  structure no_confusiongroup.homomorphism.no_confusion
81,2660
-  definition reflgroup.isomorphism.refl
158,5270
-  definition is_set_homomorphismgroup.is_set_homomorphism
106,3462
-  structure to_homgroup.isomorphism.to_hom
140,4744
-    mkgroup.isomorphism.mk
141,4777
-  theorem to_respect_onegroup.to_respect_one
97,3182
-  structure isomorphismgroup.isomorphism.rec
140,4744
-  definition transgroup.isomorphism.trans
164,5502
-  definition is_embedding_homomorphismgroup.is_embedding_homomorphism
61,2062
-  structure homomorphismgroup.homomorphism
81,2660
-  definition pmap_of_homomorphismgroup.pmap_of_homomorphism
120,3991
-  definition homomorphism_composegroup.homomorphism_compose
131,4395
-  theorem respect_invgroup.respect_inv
58,1922
-  definition group_fungroup.group_fun
87,2794
-  structure rec_ongroup.homomorphism.rec_on
81,2660
-  structure φgroup.homomorphism.φ
81,2660
-  definition homomorphism_eqgroup.homomorphism_eq
123,4120
-  definition to_is_embedding_homomorphismgroup.to_is_embedding_homomorphism
103,3330
-  definition equiv_of_isomorphismgroup.equiv_of_isomorphism
148,4976
-  structure no_confusiongroup.isomorphism.no_confusion
140,4744
-  definition symmgroup.isomorphism.symm
161,5378
-  structure destructgroup.isomorphism.destruct
140,4744
-  definition is_homomorphismgroup.is_homomorphism
39,1242
-  structure rec_ongroup.isomorphism.rec_on
140,4744
-  structure is_equiv_to_homgroup.isomorphism.is_equiv_to_hom
140,4744
-  structure isomorphismgroup.isomorphism
140,4744
-  definition homomorphism_idgroup.homomorphism_id
134,4544
-  structure homomorphismgroup.homomorphism.rec
81,2660
-  definition group_pType_of_Groupgroup.group_pType_of_Group
34,1108
-  definition respect_mulgroup.respect_mul
48,1643
-  definition pType_of_Groupgroup.pType_of_Group
24,711
-  structure cases_ongroup.homomorphism.cases_on
81,2660
-  definition is_homomorphism_composegroup.is_homomorphism_compose
72,2369
-  structure pgroup.homomorphism.p
81,2660
-  structure cases_ongroup.isomorphism.cases_on
140,4744
-
-homotopy/join_theorem.hlean,366
-    protected definition introis_conn.intro
51,1299
-  definition is_retraction_composeretraction.is_retraction_compose
11,231
-  definition is_retraction_compose_equiv_leftretraction.is_retraction_compose_equiv_left
27,703
-theorem is_conn_joinis_conn_join
70,1667
-  definition is_retraction_compose_equiv_rightretraction.is_retraction_compose_equiv_right
32,871
-
-homotopy/sec86.hlean,1825
-definition freudenthal_pequivfreudenthal_pequiv
223,8078
-  definition encode'freudenthal.encode'
121,4379
-  definition code_merid_inv_ptfreudenthal.code_merid_inv_pt
92,3441
-  definition upfreudenthal.up
58,2252
-  definition decodefreudenthal.decode
174,6391
-  definition decode_north_ptfreudenthal.decode_north_pt
115,4165
-  definition decode_coh_gfreudenthal.decode_coh_g
148,5307
-  definition psphere_succpsphere_succ
47,1992
-  theorem elim_type_merid_invelim_type_merid_inv
36,1519
-  definition decode_northfreudenthal.decode_north
112,4042
-  theorem decode_cohfreudenthal.decode_coh
160,5802
-  definition code_merid_cohfreudenthal.code_merid_coh
76,2843
-  definition equiv'freudenthal.equiv'
188,6798
-  definition decode_coh_lemfreudenthal.decode_coh_lem
156,5625
-definition freudenthal_equivfreudenthal_equiv
229,8371
-  definition is_trunc_codefreudenthal.is_trunc_code
103,3823
-  definition code_meridfreudenthal.code_merid
61,2360
-  theorem encode_decode_northfreudenthal.encode_decode_north
130,4628
-  definition is_equiv_code_meridfreudenthal.is_equiv_code_merid
81,3004
-  definition is_conn_truncis_conn_trunc
40,1776
-  definition pequiv'freudenthal.pequiv'
191,6935
-  definition decode_southfreudenthal.decode_south
118,4253
-  definition encodefreudenthal.encode
124,4469
-  definition decode_coh_ffreudenthal.decode_coh_f
139,4992
-  definition code_merid_β_leftfreudenthal.code_merid_β_left
70,2625
-  definition stability_pequivsphere.stability_pequiv
236,8573
-  definition code_merid_equivfreudenthal.code_merid_equiv
89,3312
-  definition codefreudenthal.code
100,3704
-  theorem decode_encodefreudenthal.decode_encode
182,6599
-  definition code_merid_β_rightfreudenthal.code_merid_β_right
73,2727
-  definition iterated_loop_ptrunc_pequiv_coniterated_loop_ptrunc_pequiv_con
23,1032
-
-homotopy/chain_complex.hlean,5324
-definition sintsint
36,1114
-structure carriersucc_str.carrier
24,757
-  structure mul_left_inv_ptchain_complex.pgroup.mul_left_inv_pt
478,19042
-  structure type_chain_complexchain_complex.type_chain_complex
88,3028
-  definition transfer_chain_complex2'chain_complex.transfer_chain_complex2'
336,12565
-  structure invchain_complex.pgroup.inv
478,19042
-structure no_confusionsucc_str.no_confusion
24,757
-  definition cc_to_fnchain_complex.cc_to_fn
248,9540
-  definition transfer_chain_complexchain_complex.transfer_chain_complex
280,10737
-definition stratifiedstratified
57,1945
-  structure cases_onchain_complex.chain_complex.cases_on
239,9213
-  definition is_exact_at_tchain_complex.is_exact_at_t
103,3692
-  definition whisker_left_idp_con_eq_assoceq.whisker_left_idp_con_eq_assoc
17,554
-  structure pgroupchain_complex.pgroup
478,19042
-definition stratified_succstratified_succ
53,1777
-definition snatsnat
34,955
-  definition cast_inv_castchain_complex.cast_inv_cast
178,6596
-  definition cast_cast_invchain_complex.cast_cast_inv
174,6433
-  definition is_surjective_of_trivialchain_complex.is_surjective_of_trivial
516,20301
-structure succ_strsucc_str.rec
24,757
-  structure destructchain_complex.type_chain_complex.destruct
88,3028
-  theorem is_exact_at_transferchain_complex.is_exact_at_transfer
292,11186
-  structure is_set_carrierchain_complex.pgroup.is_set_carrier
478,19042
-  structure to_has_invchain_complex.pgroup.to_has_inv
478,19042
-  definition inv_commute1'chain_complex.inv_commute1'
162,5796
-  mksucc_str.mk
25,778
-  definition is_exact_tchain_complex.is_exact_t
106,3821
-  structure cases_onchain_complex.type_chain_complex.cases_on
88,3028
-  definition tcc_to_carchain_complex.tcc_to_car
96,3299
-structure succsucc_str.succ
24,757
-  structure fnchain_complex.chain_complex.fn
239,9213
-    mkchain_complex.chain_complex.mk
240,9256
-  structure mul_assocchain_complex.pgroup.mul_assoc
478,19042
-  definition is_exact_at_truncchain_complex.is_exact_at_trunc
324,12208
-  definition is_embedding_of_trivialchain_complex.is_embedding_of_trivial
501,19848
-  definition cc_to_carchain_complex.cc_to_car
247,9473
-  definition inv_commute1chain_complex.inv_commute1
166,6045
-  definition is_equiv_of_trivialchain_complex.is_equiv_of_trivial
524,20541
-  definition is_exact_at_transfer2chain_complex.is_exact_at_transfer2
201,7632
-  definition transfer_type_chain_complexchain_complex.transfer_type_chain_complex
130,4624
-  structure rec_onchain_complex.pgroup.rec_on
478,19042
-  definition fn_cast_eq_cast_fnchain_complex.fn_cast_eq_cast_fn
170,6235
-  definition is_exact_atchain_complex.is_exact_at
254,9852
-  structure carchain_complex.type_chain_complex.car
88,3028
-definition stratified_typestratified_type
44,1365
-  structure cases_onchain_complex.pgroup.cases_on
478,19042
-  structure destructchain_complex.pgroup.destruct
478,19042
-  definition is_exact_at_transfer2'chain_complex.is_exact_at_transfer2'
357,13539
-    mkchain_complex.type_chain_complex.mk
89,3076
-  definition trunc_chain_complexchain_complex.trunc_chain_complex
312,11842
-  definition is_exactchain_complex.is_exact
257,9977
-  definition tcc_is_chain_complexchain_complex.tcc_is_chain_complex
98,3453
-definition sint'sint'
37,1193
-  structure is_chain_complexchain_complex.chain_complex.is_chain_complex
239,9213
-  definition group_of_pgroupchain_complex.group_of_pgroup
483,19228
-  structure chain_complexchain_complex.chain_complex
239,9213
-  structure chain_complexchain_complex.chain_complex.rec
239,9213
-  definition cc_is_chain_complexchain_complex.cc_is_chain_complex
249,9618
-  structure type_chain_complexchain_complex.type_chain_complex.rec
88,3028
-  structure no_confusionchain_complex.type_chain_complex.no_confusion
88,3028
-definition snat'snat'
35,1034
-  structure destructchain_complex.chain_complex.destruct
239,9213
-  structure mul_ptchain_complex.pgroup.mul_pt
478,19042
-  structure pgroupchain_complex.pgroup.rec
478,19042
-  structure carchain_complex.chain_complex.car
239,9213
-  structure fnchain_complex.type_chain_complex.fn
88,3028
-definition Ssucc_str.S
30,875
-  structure is_chain_complexchain_complex.type_chain_complex.is_chain_complex
88,3028
-  structure mulchain_complex.pgroup.mul
478,19042
-structure cases_onsucc_str.cases_on
24,757
-  definition transfer_type_chain_complex2chain_complex.transfer_type_chain_complex2
183,6842
-    mkchain_complex.pgroup.mk
479,19107
-  definition pgroup_of_groupchain_complex.pgroup_of_group
491,19482
-structure rec_onsucc_str.rec_on
24,757
-  definition tcc_to_fnchain_complex.tcc_to_fn
97,3372
-  structure rec_onchain_complex.type_chain_complex.rec_on
88,3028
-  structure no_confusionchain_complex.pgroup.no_confusion
478,19042
-  theorem is_exact_at_t_transferchain_complex.is_exact_at_t_transfer
142,5091
-  structure rec_onchain_complex.chain_complex.rec_on
239,9213
-structure succ_strsucc_str
24,757
-  definition is_trunc_ptrunctypechain_complex.is_trunc_ptrunctype
473,18817
-  structure to_semigroupchain_complex.pgroup.to_semigroup
478,19042
-structure destructsucc_str.destruct
24,757
-  definition transport_eq_Fl_idp_lefteq.transport_eq_Fl_idp_left
13,386
-  structure no_confusionchain_complex.chain_complex.no_confusion
239,9213
-  structure pt_mulchain_complex.pgroup.pt_mul
478,19042
-
-homotopy/spectrum.hlean,5800
-structure is_spectrumis_spectrum.rec
187,9094
-structure destructgen_spectrum.destruct
192,9275
-  definition pequiv_postcomposepointed.pequiv_postcompose
137,7133
-structure no_confusiongen_prespectrum.no_confusion
181,8929
-structure gluegen_prespectrum.glue
181,8929
-  structure cases_onspectrum.sp_chain_complex.cases_on
386,18262
-  structure no_confusionspectrum.sp_chain_complex.no_confusion
386,18262
-  definition pequiv_precomposepointed.pequiv_precompose
145,7584
-  definition loop_pmap_commutepointed.loop_pmap_commute
73,2970
-abbreviation mkspectrum.mk
203,9684
-  definition psp_of_gen_indexedspectrum.psp_of_gen_indexed
248,11436
-  structure shomotopyspectrum.shomotopy
317,15315
-  structure shomotopyspectrum.shomotopy.rec
317,15315
-structure destructgen_prespectrum.destruct
181,8929
-  structure fnspectrum.sp_chain_complex.fn
386,18262
-    definition scc_to_carspectrum.scc_to_car
394,18517
-  structure sp_chain_complexspectrum.sp_chain_complex
386,18262
-  structure carspectrum.sp_chain_complex.car
386,18262
-  protected definition of_gen_indexedspectrum.of_gen_indexed
257,11975
-  definition shomotopy_groupspectrum.shomotopy_group
356,16961
-structure cases_onis_spectrum.cases_on
187,9094
-structure cases_ongen_spectrum.cases_on
192,9275
-  structure rec_onspectrum.sp_chain_complex.rec_on
386,18262
-  mkgen_prespectrum.mk
182,8965
-  definition ppcompose_leftpointed.ppcompose_left
82,3567
-structure no_confusionis_spectrum.no_confusion
187,9094
-  definition scomposespectrum.scompose
299,14044
-structure to_prespectrumgen_spectrum.to_prespectrum
192,9275
-  structure no_confusionspectrum.smap.no_confusion
278,13041
-  definition szerospectrum.szero
311,14839
-  structure cases_onspectrum.smap.cases_on
278,13041
-structure gen_prespectrumgen_prespectrum.rec
181,8929
-  structure no_confusionspectrum.shomotopy.no_confusion
317,15315
-abbreviation spectrumspectrum
202,9643
-  structure cases_onspectrum.shomotopy.cases_on
317,15315
-    definition scc_is_chain_complexspectrum.scc_is_chain_complex
396,18670
-  definition struncspectrum.strunc
343,16403
-  structure glue_squarespectrum.smap.glue_square
278,13041
-structure destructis_spectrum.destruct
187,9094
-  structure smapspectrum.smap.rec
278,13041
-  definition pfiber_loop_spacepointed.pfiber_loop_space
110,5185
-  definition pequiv_composepointed.pequiv_compose
35,1119
-  definition psuspnspectrum.psuspn
330,15866
-  definition pmap_eq_equivpointed.pmap_eq_equiv
58,1870
-structure deloopgen_prespectrum.deloop
181,8929
-  structure rec_onspectrum.shomotopy.rec_on
317,15315
-  definition transport_fiber_equivpointed.transport_fiber_equiv
132,6798
-  definition pcompose_pconstpointed.pcompose_pconst
101,4763
-  mkis_spectrum.mk
188,9158
-  definition sglue_squarespectrum.sglue_square
288,13371
-  definition equiv_ppcompose_leftpointed.equiv_ppcompose_left
98,4631
-  definition ap1_pconstpointed.ap1_pconst
107,5048
-  definition ppipointed.ppi
160,8279
-  structure glue_homotopyspectrum.shomotopy.glue_homotopy
317,15315
-structure rec_ongen_spectrum.rec_on
192,9275
-  definition sigma_equiv_sigma_left'sigma.sigma_equiv_sigma_left'
20,711
-  definition is_spectrum_of_gen_indexedspectrum.is_spectrum_of_gen_indexed
251,11679
-  structure to_funspectrum.smap.to_fun
278,13041
-  definition pfiber_equiv_of_phomotopypointed.pfiber_equiv_of_phomotopy
121,6291
-  structure destructspectrum.sp_chain_complex.destruct
386,18262
-structure gen_spectrumgen_spectrum.rec
192,9275
-  protected definition of_nat_indexedspectrum.of_nat_indexed
237,10937
-  protected definition MKspectrum.MK
262,12282
-  definition equiv_ppi_rightpointed.equiv_ppi_right
166,8498
-    definition scc_to_fnspectrum.scc_to_fn
395,18590
-structure rec_onis_spectrum.rec_on
187,9094
-  structure destructspectrum.shomotopy.destruct
317,15315
-structure gen_prespectrumgen_prespectrum
181,8929
-  definition is_spectrum_of_nat_indexedspectrum.is_spectrum_of_nat_indexed
230,10636
-  protected definition Mkspectrum.Mk
270,12731
-  definition equiv_gluespectrum.equiv_glue
209,9865
-    mkspectrum.smap.mk
279,13094
-  mkgen_spectrum.mk
193,9308
-structure is_equiv_glueis_spectrum.is_equiv_glue
187,9094
-  definition gluespectrum.glue
207,9753
-  definition sigma_charpointed.phomotopy.sigma_char
49,1559
-  structure sp_chain_complexspectrum.sp_chain_complex.rec
386,18262
-  structure smapspectrum.smap
278,13041
-    mkspectrum.shomotopy.mk
318,15388
-structure gen_spectrumgen_spectrum
192,9275
-  definition psp_suspspectrum.psp_susp
335,16065
-structure is_spectrumis_spectrum
187,9094
-  structure is_chain_complexspectrum.sp_chain_complex.is_chain_complex
386,18262
-structure cases_ongen_prespectrum.cases_on
181,8929
-  definition sfiberspectrum.sfiber
382,18050
-  definition of_natspectrum.succ_str.of_nat
244,11289
-  definition pathover_eq_Fl'eq.pathover_eq_Fl'
28,913
-structure rec_ongen_prespectrum.rec_on
181,8929
-  definition pconst_pcomposepointed.pconst_pcompose
104,4907
-structure no_confusiongen_spectrum.no_confusion
192,9275
-  structure rec_onspectrum.smap.rec_on
278,13041
-    mkspectrum.sp_chain_complex.mk
387,18308
-  definition sp_cotensorspectrum.sp_cotensor
366,17352
-  definition pfiber_equiv_of_squarepointed.pfiber_equiv_of_square
154,7944
-  structure destructspectrum.smap.destruct
278,13041
-  definition loop_ppi_commutepointed.loop_ppi_commute
163,8361
-  definition sidspectrum.sid
293,13688
-  structure to_phomotopyspectrum.shomotopy.to_phomotopy
317,15315
-structure to_is_spectrumgen_spectrum.to_is_spectrum
192,9275
-  definition psp_of_nat_indexedspectrum.psp_of_nat_indexed
216,10207
-  definition spispectrum.spi
374,17699
-  definition sigma_charpointed.pmap.sigma_char
40,1292
-  definition is_equiv_ppcompose_leftpointed.is_equiv_ppcompose_left
85,3741
-
-algebra/module.hlean,3083
-mkleft_module.mk
22,563
-structure destructleft_module.destruct
20,467
-structure cases_onvector_space.cases_on
72,2518
-  proposition smul_zerosmul_zero
50,1651
-structure rec_onleft_module.rec_on
20,467
-structure mul_smulleft_module.mul_smul
20,467
-  proposition neg_one_smulneg_one_smul
57,1961
-structure has_scalarhas_scalar
13,339
-structure smul_left_distribvector_space.smul_left_distrib
72,2518
-structure add_zerovector_space.add_zero
72,2518
-structure cases_onhas_scalar.cases_on
13,339
-  proposition one_smulone_smul
44,1413
-structure zero_addleft_module.zero_add
20,467
-structure rec_onhas_scalar.rec_on
13,339
-structure smulvector_space.smul
72,2518
-structure addvector_space.add
72,2518
-structure smul_left_distribleft_module.smul_left_distrib
20,467
-structure left_moduleleft_module.rec
20,467
-  proposition mul_smulmul_smul
41,1310
-  proposition smul_left_distribsmul_left_distrib
35,1074
-structure destructhas_scalar.destruct
13,339
-structure smulleft_module.smul
20,467
-structure negleft_module.neg
20,467
-structure vector_spacevector_space
72,2518
-  proposition smul_negsmul_neg
60,2054
-structure one_smulleft_module.one_smul
20,467
-structure is_set_carrierleft_module.is_set_carrier
20,467
-structure left_moduleleft_module
20,467
-structure no_confusionleft_module.no_confusion
20,467
-  proposition neg_smulneg_smul
54,1811
-structure no_confusionhas_scalar.no_confusion
13,339
-structure destructvector_space.destruct
72,2518
-structure add_commvector_space.add_comm
72,2518
-structure mkvector_space.mk
72,2518
-structure zero_addvector_space.zero_add
72,2518
-structure zerovector_space.zero
72,2518
-structure add_zeroleft_module.add_zero
20,467
-structure smul_right_distribvector_space.smul_right_distrib
72,2518
-  proposition zero_smulzero_smul
46,1488
-structure vector_spacevector_space.rec
72,2518
-structure negvector_space.neg
72,2518
-structure has_scalarhas_scalar.rec
13,339
-structure add_assocvector_space.add_assoc
72,2518
-structure one_smulvector_space.one_smul
72,2518
-structure add_assocleft_module.add_assoc
20,467
-  proposition sub_smul_right_distribsub_smul_right_distrib
66,2336
-structure zeroleft_module.zero
20,467
-structure smul_right_distribleft_module.smul_right_distrib
20,467
-  proposition smul_right_distribsmul_right_distrib
38,1191
-structure add_commleft_module.add_comm
20,467
-structure is_set_carriervector_space.is_set_carrier
72,2518
-structure add_left_invvector_space.add_left_inv
72,2518
-structure cases_onleft_module.cases_on
20,467
-structure rec_onvector_space.rec_on
72,2518
-structure no_confusionvector_space.no_confusion
72,2518
-  proposition smul_sub_left_distribsmul_sub_left_distrib
63,2189
-structure smulhas_scalar.smul
13,339
-structure to_add_comm_groupleft_module.to_add_comm_group
20,467
-structure mul_smulvector_space.mul_smul
72,2518
-structure add_left_invleft_module.add_left_inv
20,467
-mkhas_scalar.mk
14,374
-structure addleft_module.add
20,467
-structure to_left_modulevector_space.to_left_module
72,2518
-structure to_has_scalarleft_module.to_has_scalar
20,467
diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index b2ae55b..5d514f0 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -123,11 +123,12 @@ namespace group
     (is_normal_subgroup : is_normal R)
 
   attribute subgroup_rel.R [coercion]
-  abbreviation subgroup_to_rel      [unfold 2] := @subgroup_rel.R
-  abbreviation subgroup_has_one     [unfold 2] := @subgroup_rel.Rone
-  abbreviation subgroup_respect_mul [unfold 2] := @subgroup_rel.Rmul
-  abbreviation subgroup_respect_inv [unfold 2] := @subgroup_rel.Rinv
-  abbreviation is_normal_subgroup   [unfold 2] := @normal_subgroup_rel.is_normal_subgroup
+  abbreviation subgroup_to_rel      [parsing_only] [unfold 2] := @subgroup_rel.R
+  abbreviation subgroup_has_one     [parsing_only] [unfold 2] := @subgroup_rel.Rone
+  abbreviation subgroup_respect_mul [parsing_only] [unfold 2] := @subgroup_rel.Rmul
+  abbreviation subgroup_respect_inv [parsing_only] [unfold 2] := @subgroup_rel.Rinv
+  abbreviation is_normal_subgroup   [parsing_only] [unfold 2] :=
+  @normal_subgroup_rel.is_normal_subgroup
 
   variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
             {A B : CommGroup}
diff --git a/homotopy/smash.hlean b/homotopy/smash.hlean
index c7cc0e3..7d6e2fc 100644
--- a/homotopy/smash.hlean
+++ b/homotopy/smash.hlean
@@ -6,9 +6,9 @@
   However, we define it (equivalently) as the pushout of the maps A + B → 2 and A + B → A × B.
 -/
 
-import homotopy.circle homotopy.join types.pointed ..move_to_lib
+import homotopy.circle homotopy.join types.pointed homotopy.cofiber ..move_to_lib
 
-open bool pointed eq equiv is_equiv sum bool prod unit circle
+open bool pointed eq equiv is_equiv sum bool prod unit circle cofiber
 
 namespace smash
 
@@ -181,6 +181,38 @@ namespace smash
 
   /- To prove: commutative, associative -/
 
+  /- smash A B ≃ pcofiber (pprod_of_pwedge A B) -/
+
+  definition prod_of_pwedge [unfold 3] (v : pwedge A B) : A × B :=
+  begin
+    induction v with a b ,
+    { exact (a, pt) },
+    { exact (pt, b) },
+    { reflexivity }
+  end
+
+  definition pprod_of_pwedge [constructor] : pwedge A B →* A ×* B :=
+  begin
+    fconstructor,
+    { intro v, induction v with a b ,
+      { exact (a, pt) },
+      { exact (pt, b) },
+      { reflexivity }},
+    { reflexivity }
+  end
+
+  attribute pcofiber [constructor]
+  definition pcofiber_of_smash (x : smash A B) : pcofiber (@pprod_of_pwedge A B) :=
+  begin
+    induction x,
+    { exact pushout.inr (a, b) },
+    { exact pushout.inl ⋆ },
+    { exact pushout.inl ⋆ },
+    { symmetry, },
+    { }
+  end
+
+
   /- smash A S¹ = susp A -/
   open susp
 
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 4243431..6de864b 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -7,7 +7,7 @@ open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc
 
 attribute equiv.symm equiv.trans is_equiv.is_equiv_ap fiber.equiv_postcompose
           fiber.equiv_precompose pequiv.to_pmap pequiv._trans_of_to_pmap ghomotopy_group_succ_in
-          isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv
+          isomorphism_of_eq pmap_bool_equiv sphere_equiv_bool psphere_pequiv_pbool fiber_eq_equiv int.equiv_succ
           [constructor]
 attribute is_equiv.eq_of_fn_eq_fn' [unfold 3]
 attribute isomorphism._trans_of_to_hom [unfold 3]
@@ -25,6 +25,21 @@ open sigma
 namespace group
   open is_trunc
 
+  -- some extra instances for type class inference
+  definition is_homomorphism_comm_homomorphism [instance] {G G' : CommGroup} (φ : G →g G')
+    : @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G))
+                            (@comm_group.to_group _ (CommGroup.struct G')) φ :=
+  homomorphism.struct φ
+
+  definition is_homomorphism_comm_homomorphism1 [instance] {G G' : CommGroup} (φ : G →g G')
+    : @is_homomorphism G G' _
+                            (@comm_group.to_group _ (CommGroup.struct G')) φ :=
+  homomorphism.struct φ
+
+  definition is_homomorphism_comm_homomorphism2 [instance] {G G' : CommGroup} (φ : G →g G')
+    : @is_homomorphism G G' (@comm_group.to_group _ (CommGroup.struct G)) _ φ :=
+  homomorphism.struct φ
+
   theorem inv_eq_one {A : Type} [group A] {a : A} (H : a = 1) : a⁻¹ = 1 :=
   iff.mpr (inv_eq_one_iff_eq_one a) H