Duplication · anthropics/fermats-last-theorem

Duplication Overall

47% duplication:

5,889,107 cleaned lines of cleaned code (without empty lines, comments, and frequently duplicated constructs such as imports)
2,826,080 duplicated lines

645,964 duplicates

dependency graphs: 2D graph | 2D graph (with duplicates)... | 3D graph | 3D graph (with duplicates)...

Duplication per Extension

Duplication per Component (primary)

Duplication Between Components (50+ lines)

flowchart TB
    n0["P2M"]
    n1["Theorems"]
    n2["Definitions"]
    n3["html"]
    n4["tools"]
    n0 ---|"566749"| n1
    n2 ---|"67976"| n0
    n2 ---|"5580"| n1
    n3 ---|"1340"| n4
    classDef default fill:#00b2ee,stroke:#ffffff,color:#000000;
    classDef highlighted fill:#00b2ee,stroke:#ffffff,color:#000000;
    linkStyle 0 stroke:#DC143CFF,stroke-width:10px
    linkStyle 1 stroke:#DC143C5E,stroke-width:1px
    linkStyle 2 stroke:#DC143C4C,stroke-width:1px
    linkStyle 3 stroke:#DC143C4C,stroke-width:1px

Download: Mermaid (.mmd) (open online Mermaid editor)

2D force graph | 3D force graph

Show more details on duplication between components...

From Component --> To Component	Duplicated Lines	File Pairs	Details
P2M (5%) --> Theorems (64%)	566749	129590 file pairs	details...
Definitions (15%) --> P2M (<1%)	67976	2332 file pairs	details...
Definitions (1%) --> Theorems (<1%)	5580	846 file pairs	details...
html (24%) --> tools (28%)	1340	4 file pairs	details...

Longest Duplicates

The list of 50 longest duplicates.

See data for all 645,964 duplicates...

Size	#	Folders	Files	Lines	Code
4230	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	11:4794 (94%) 10:4793 (93%)	view
2805	x 2	P2M/Sol P2M/Sol	lean S_AutomorphicForm_exists_analyticOnNh... S_AutomorphicForm_exists_analyticOnNh...	105:3246 (46%) 105:3246 (45%)	view
2514	x 2	P2M/Sol P2M/Sol	lean S_ModularCurve_B3_exists_variableChan... S_ModularCurve_B3_isElliptic_specialF...	26:2804 (98%) 26:2804 (98%)	view
2499	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	1954:4793 (55%) 1958:4797 (47%)	view
2499	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	1955:4794 (55%) 1958:4797 (47%)	view
2268	x 2	P2M/Sol P2M/Sol	lean S_NumberField_Idele_continuous_semiLo... S_TwistedUnipotentTerm_exists_transve...	41:2558 (90%) 32:2549 (48%)	view
2268	x 2	P2M/Sol P2M/Sol	lean S_NumberField_Idele_continuous_semiLo... S_NumberField_Idele_secondCountableTo...	41:2558 (90%) 32:2549 (90%)	view
2268	x 2	P2M/Sol P2M/Sol	lean S_NumberField_Idele_secondCountableTo... S_TwistedUnipotentTerm_exists_transve...	32:2549 (90%) 32:2549 (48%)	view
2135	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_exists_ar...	2365:4794 (47%) 2362:4791 (47%)	view
2135	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_exists_ar...	2368:4797 (40%) 2362:4791 (47%)	view
2135	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_exists_ar...	2364:4793 (47%) 2362:4791 (47%)	view
2092	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_exists_ar...	11:2359 (46%) 9:2357 (46%)	view
2092	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_exists_ar...	10:2358 (46%) 9:2357 (46%)	view
2069	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_CubicInduction_con... S_LanglandsTunnell_CubicInduction_exi...	49:2498 (96%) 49:2498 (96%)	view
2039	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	10:2297 (39%) 11:2298 (39%)	view
2037	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_exists_ar...	14:2297 (39%) 11:2294 (45%)	view
2037	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	12:2295 (45%) 15:2298 (39%)	view
2037	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	13:2296 (45%) 14:2297 (39%)	view
2037	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_exists_ar...	15:2298 (39%) 11:2294 (45%)	view
2037	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	12:2295 (45%) 14:2297 (39%)	view
2037	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	13:2296 (45%) 15:2298 (39%)	view
1931	x 2	P2M/Sol P2M/Sol	lean S_ModularCurve_UVCrossingModel_exists... S_ModularCurve_UVCrossingModel_exists...	18:2218 (81%) 18:2218 (82%)	view
1931	x 2	P2M/Sol P2M/Sol	lean S_ModularCurve_UVCrossingModel_exists... S_ModularCurve_UVCrossingModel_exists...	18:2218 (81%) 19:2219 (85%)	view
1931	x 2	P2M/Sol P2M/Sol	lean S_ModularCurve_UVCrossingModel_exists... S_ModularCurve_UVCrossingModel_exists...	19:2219 (85%) 18:2218 (82%)	view
1901	x 2	P2M/Sol P2M/Sol	lean S_RegularSingular_exists_logDepth_le_... S_RegularSingular_exists_norm_apply_l...	20:2135 (47%) 20:2135 (45%)	view
1901	x 2	P2M/Sol P2M/Sol	lean S_RegularSingular_exists_const_norm_a... S_RegularSingular_exists_logDepth_le_...	20:2135 (60%) 20:2135 (47%)	view
1901	x 2	P2M/Sol P2M/Sol	lean S_RegularSingular_exists_const_norm_a... S_RegularSingular_exists_norm_apply_l...	20:2135 (60%) 20:2135 (45%)	view
1806	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_ArchDatum... S_LanglandsTunnell_Converse_ArchDatum...	28:2054 (36%) 26:2052 (36%)	view
1730	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	11:1952 (32%) 11:1952 (33%)	view
1730	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	10:1951 (33%) 11:1952 (32%)	view
1728	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	12:1949 (38%) 15:1952 (32%)	view
1728	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	13:1950 (38%) 15:1952 (32%)	view
1728	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_exists_ar...	15:1952 (32%) 11:1948 (38%)	view
1703	x 2	P2M/Sol P2M/Sol	lean S_NumberField_LevelArith_exists_conti... S_NumberField_LevelArith_exists_conti...	24:2003 (95%) 24:2003 (82%)	view
1600	x 2	P2M/Sol P2M/Sol	lean S_ModularCurve_B3_b3_specialisationEq... S_ModularCurve_B3_specialisationEquiv...	108:1874 (73%) 110:1876 (73%)	view
1594	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_CubicInduction_int... S_LanglandsTunnell_CubicInduction_jac...	31:1772 (85%) 34:1775 (89%)	view
1525	x 2	P2M/Sol P2M/Sol	lean S_rademacher_phi_level_witness_eleven... S_rademacher_phi_level_witness_mod_si...	12:1621 (99%) 12:1621 (99%)	view
1525	x 2	P2M/Sol P2M/Sol	lean S_rademacher_phi_level_witness_mod_si... S_rademacher_phi_level_witness_seven....	12:1621 (99%) 12:1621 (99%)	view
1525	x 2	P2M/Sol P2M/Sol	lean S_rademacher_phi_level_witness_mod_si... S_rademacher_phi_level_witness_seven....	12:1621 (99%) 12:1621 (99%)	view
1525	x 2	P2M/Sol P2M/Sol	lean S_rademacher_phi_level_witness_eleven... S_rademacher_phi_level_witness_mod_si...	12:1621 (99%) 12:1621 (99%)	view
1525	x 2	P2M/Sol P2M/Sol	lean S_rademacher_phi_level_witness_mod_si... S_rademacher_phi_level_witness_mod_si...	12:1621 (99%) 12:1621 (99%)	view
1525	x 2	P2M/Sol P2M/Sol	lean S_rademacher_phi_level_witness_eleven... S_rademacher_phi_level_witness_seven....	12:1621 (99%) 12:1621 (99%)	view
1525	x 2	P2M/Sol P2M/Sol	lean S_rademacher_phi_level_witness_five.lean S_rademacher_phi_level_witness_mod_si...	12:1621 (99%) 12:1621 (99%)	view
1525	x 2	P2M/Sol P2M/Sol	lean S_rademacher_phi_level_witness_five.lean S_rademacher_phi_level_witness_seven....	12:1621 (99%) 12:1621 (99%)	view
1525	x 2	P2M/Sol P2M/Sol	lean S_rademacher_phi_level_witness_eleven... S_rademacher_phi_level_witness_five.lean	12:1621 (99%) 12:1621 (99%)	view
1525	x 2	P2M/Sol P2M/Sol	lean S_rademacher_phi_level_witness_five.lean S_rademacher_phi_level_witness_mod_si...	12:1621 (99%) 12:1621 (99%)	view
1516	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_exists_ar...	3092:4795 (29%) 3088:4791 (33%)	view
1516	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	3090:4793 (33%) 3094:4797 (29%)	view
1516	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	3091:4794 (33%) 3092:4795 (29%)	view
1516	x 2	P2M/Sol P2M/Sol	lean S_LanglandsTunnell_Converse_Principal... S_LanglandsTunnell_Converse_Principal...	3094:4797 (28%) 3094:4797 (29%)	view

Most Frequent Duplicates

The list of 50 most frequently found duplicates.

Size	#	Folders	Files	Lines	Code
6	x 270	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems Theorems P2M/Sol ...	lean S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_fin... Thm_ModularCurve_FullLevel_AuxLevel_c... S_ModularCurve_FullLevel_AuxLevel_blo... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_b... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_exi... ...	80:85 (1%) 71:76 (3%) 338:343 (1%) 77:82 (7%) 156:161 (1%) 188:193 (1%) 74:79 (2%) 71:76 (2%) 187:192 (1%) 73:78 (2%) ...	view
6	x 270	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems Theorems P2M/Sol ...	lean S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_fin... Thm_ModularCurve_FullLevel_AuxLevel_c... S_ModularCurve_FullLevel_AuxLevel_blo... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_b... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_exi... ...	83:88 (1%) 74:79 (3%) 341:346 (1%) 80:85 (7%) 159:164 (1%) 191:196 (1%) 77:82 (2%) 74:79 (2%) 190:195 (1%) 76:81 (2%) ...	view
6	x 270	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems Theorems P2M/Sol ...	lean S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_fin... Thm_ModularCurve_FullLevel_AuxLevel_c... S_ModularCurve_FullLevel_AuxLevel_blo... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_b... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_exi... ...	82:87 (1%) 73:78 (3%) 340:345 (1%) 79:84 (7%) 158:163 (1%) 190:195 (1%) 76:81 (2%) 73:78 (2%) 189:194 (1%) 75:80 (2%) ...	view
6	x 270	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems Theorems P2M/Sol ...	lean S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_fin... Thm_ModularCurve_FullLevel_AuxLevel_c... S_ModularCurve_FullLevel_AuxLevel_blo... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_b... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_exi... ...	79:84 (1%) 70:75 (3%) 337:342 (1%) 76:81 (7%) 155:160 (1%) 187:192 (1%) 73:78 (2%) 70:75 (2%) 186:191 (1%) 72:77 (2%) ...	view
6	x 270	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems Theorems P2M/Sol ...	lean S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_fin... Thm_ModularCurve_FullLevel_AuxLevel_c... S_ModularCurve_FullLevel_AuxLevel_blo... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_b... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_exi... ...	81:86 (1%) 72:77 (3%) 339:344 (1%) 78:83 (7%) 157:162 (1%) 189:194 (1%) 75:80 (2%) 72:77 (2%) 188:193 (1%) 74:79 (2%) ...	view
6	x 247	P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol ...	lean S_CerednikDrinfeld_FormalOmega_exists... S_CerednikDrinfeld_awayUnits_exists_c... S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_UnramQuad_free_f... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_FakeEllipticCur... S_CerednikDrinfeld_exists_disc_holOn_... S_CerednikDrinfeld_QM_FakeEllipticCur... S_CerednikDrinfeld_ringHom_functionFi... ...	17:22 (18%) 259:264 (2%) 269:274 (1%) 17:22 (27%) 103:108 (1%) 537:542 (<1%) 137:142 (1%) 50:55 (1%) 86:91 (3%) 286:291 (1%) ...	view
6	x 236	Theorems Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems ...	lean Thm_ModularCurve_FullLevel_coe_chartA... Thm_ModularCurve_FullLevel_map_jChart... S_ModularCurve_FullLevel_coe_chartAlg... S_ModularCurve_FullLevel_supersingula... S_ModularCurve_FullLevel_exists_fullL... S_ModularCurve_FullLevel_forall_tubeB... S_ModularCurve_FullLevel_exists_admis... Thm_ModularCurve_FullLevel_exists_adm... Thm_ModularCurve_FullLevel_exists_ful... Thm_ModularCurve_FullLevel_exists_rea... ...	30:35 (4%) 31:36 (5%) 240:245 (1%) 263:268 (<1%) 649:654 (<1%) 34:39 (4%) 174:179 (2%) 25:30 (5%) 32:37 (5%) 32:37 (4%) ...	view
6	x 234	Theorems Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems ...	lean Thm_ModularCurve_FullLevel_coe_chartA... Thm_ModularCurve_FullLevel_map_jChart... S_ModularCurve_FullLevel_coe_chartAlg... S_ModularCurve_FullLevel_supersingula... S_ModularCurve_FullLevel_exists_fullL... S_ModularCurve_FullLevel_forall_tubeB... S_ModularCurve_FullLevel_exists_admis... Thm_ModularCurve_FullLevel_exists_adm... Thm_ModularCurve_FullLevel_exists_ful... Thm_ModularCurve_FullLevel_exists_rea... ...	29:34 (4%) 30:35 (5%) 239:244 (1%) 262:267 (<1%) 648:653 (<1%) 33:38 (4%) 173:178 (2%) 24:29 (5%) 31:36 (5%) 31:36 (4%) ...	view
6	x 234	Theorems Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems ...	lean Thm_ModularCurve_FullLevel_coe_chartA... Thm_ModularCurve_FullLevel_map_jChart... S_ModularCurve_FullLevel_coe_chartAlg... S_ModularCurve_FullLevel_supersingula... S_ModularCurve_FullLevel_exists_fullL... S_ModularCurve_FullLevel_forall_tubeB... S_ModularCurve_FullLevel_exists_admis... Thm_ModularCurve_FullLevel_exists_adm... Thm_ModularCurve_FullLevel_exists_ful... Thm_ModularCurve_FullLevel_exists_rea... ...	28:33 (4%) 29:34 (5%) 238:243 (1%) 261:266 (<1%) 647:652 (<1%) 32:37 (4%) 172:177 (2%) 23:28 (5%) 30:35 (5%) 30:35 (4%) ...	view
6	x 234	Theorems Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems ...	lean Thm_ModularCurve_FullLevel_coe_chartA... Thm_ModularCurve_FullLevel_map_jChart... S_ModularCurve_FullLevel_coe_chartAlg... S_ModularCurve_FullLevel_supersingula... S_ModularCurve_FullLevel_exists_fullL... S_ModularCurve_FullLevel_forall_tubeB... S_ModularCurve_FullLevel_exists_admis... Thm_ModularCurve_FullLevel_exists_adm... Thm_ModularCurve_FullLevel_exists_ful... Thm_ModularCurve_FullLevel_exists_rea... ...	27:32 (4%) 28:33 (5%) 237:242 (1%) 260:265 (<1%) 646:651 (<1%) 31:36 (4%) 171:176 (2%) 22:27 (5%) 29:34 (5%) 29:34 (4%) ...	view
6	x 230	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	4:9 (<1%) 4:9 (7%) 4:9 (5%) 4:9 (10%) 4:9 (1%) 4:9 (1%) 4:9 (<1%) 4:9 (10%) 4:9 (4%) 4:9 (8%) ...	view
6	x 230	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	3:8 (<1%) 3:8 (7%) 3:8 (5%) 3:8 (10%) 3:8 (1%) 3:8 (1%) 3:8 (<1%) 3:8 (10%) 3:8 (4%) 3:8 (8%) ...	view
6	x 230	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	5:10 (<1%) 5:10 (7%) 5:10 (5%) 5:10 (10%) 5:10 (1%) 5:10 (1%) 5:10 (<1%) 5:10 (10%) 5:10 (4%) 5:10 (8%) ...	view
6	x 230	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	6:11 (<1%) 6:11 (7%) 6:11 (5%) 6:11 (10%) 6:11 (1%) 6:11 (1%) 6:11 (<1%) 6:11 (10%) 6:11 (4%) 6:11 (8%) ...	view
6	x 215	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	9:14 (<1%) 9:14 (7%) 9:14 (5%) 9:14 (10%) 9:14 (1%) 9:14 (1%) 9:14 (<1%) 9:14 (10%) 9:14 (4%) 9:14 (8%) ...	view
6	x 215	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	14:19 (<1%) 14:19 (7%) 14:19 (5%) 14:19 (10%) 14:19 (1%) 14:19 (1%) 14:19 (<1%) 14:19 (10%) 14:19 (4%) 14:19 (8%) ...	view
6	x 215	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	11:16 (<1%) 11:16 (7%) 11:16 (5%) 11:16 (10%) 11:16 (1%) 11:16 (1%) 11:16 (<1%) 11:16 (10%) 11:16 (4%) 11:16 (8%) ...	view
6	x 215	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	12:17 (<1%) 12:17 (7%) 12:17 (5%) 12:17 (10%) 12:17 (1%) 12:17 (1%) 12:17 (<1%) 12:17 (10%) 12:17 (4%) 12:17 (8%) ...	view
6	x 215	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	15:20 (<1%) 15:20 (7%) 15:20 (5%) 15:20 (10%) 15:20 (1%) 15:20 (1%) 15:20 (<1%) 15:20 (10%) 15:20 (4%) 15:20 (8%) ...	view
6	x 215	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	13:18 (<1%) 13:18 (7%) 13:18 (5%) 13:18 (10%) 13:18 (1%) 13:18 (1%) 13:18 (<1%) 13:18 (10%) 13:18 (4%) 13:18 (8%) ...	view
6	x 215	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	8:13 (<1%) 8:13 (7%) 8:13 (5%) 8:13 (10%) 8:13 (1%) 8:13 (1%) 8:13 (<1%) 8:13 (10%) 8:13 (4%) 8:13 (8%) ...	view
6	x 215	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	10:15 (<1%) 10:15 (7%) 10:15 (5%) 10:15 (10%) 10:15 (1%) 10:15 (1%) 10:15 (<1%) 10:15 (10%) 10:15 (4%) 10:15 (8%) ...	view
6	x 214	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	2:7 (<1%) 2:7 (7%) 2:7 (5%) 2:7 (10%) 2:7 (1%) 2:7 (1%) 2:7 (<1%) 2:7 (10%) 2:7 (4%) 2:7 (8%) ...	view
6	x 214	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	1:6 (<1%) 1:6 (7%) 1:6 (5%) 1:6 (10%) 1:6 (1%) 1:6 (1%) 1:6 (<1%) 1:6 (10%) 1:6 (4%) 1:6 (8%) ...	view
6	x 214	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_TateLocal_exists... S_LanglandsTunnell_RankinSelberg_gode... Thm_AutomorphicForm_WhittakerModel_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_fora... S_LanglandsTunnell_RankinSelberg_rsLo... Thm_LanglandsTunnell_CubicInduction_g... S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... ...	7:12 (<1%) 7:12 (7%) 7:12 (5%) 7:12 (10%) 7:12 (1%) 7:12 (1%) 7:12 (<1%) 7:12 (10%) 7:12 (4%) 7:12 (8%) ...	view
6	x 205	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems ...	lean S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_UnramQuad_free_f... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_FakeEllipticCur... S_CerednikDrinfeld_exists_disc_holOn_... S_CerednikDrinfeld_QM_FakeEllipticCur... S_CerednikDrinfeld_ringHom_functionFi... S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_FormalOmega_desc... ...	265:271 (1%) 13:19 (27%) 99:105 (1%) 533:539 (<1%) 133:139 (1%) 46:52 (1%) 82:88 (3%) 282:288 (1%) 57:63 (3%) 19:25 (5%) ...	view
6	x 205	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems ...	lean S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_UnramQuad_free_f... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_FakeEllipticCur... S_CerednikDrinfeld_exists_disc_holOn_... S_CerednikDrinfeld_QM_FakeEllipticCur... S_CerednikDrinfeld_ringHom_functionFi... S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_FormalOmega_desc... ...	267:273 (1%) 15:21 (27%) 101:107 (1%) 535:541 (<1%) 135:141 (1%) 48:54 (1%) 84:90 (3%) 284:290 (1%) 59:65 (3%) 21:27 (5%) ...	view
6	x 205	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems ...	lean S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_UnramQuad_free_f... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_FakeEllipticCur... S_CerednikDrinfeld_exists_disc_holOn_... S_CerednikDrinfeld_QM_FakeEllipticCur... S_CerednikDrinfeld_ringHom_functionFi... S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_FormalOmega_desc... ...	266:272 (1%) 14:20 (27%) 100:106 (1%) 534:540 (<1%) 134:140 (1%) 47:53 (1%) 83:89 (3%) 283:289 (1%) 58:64 (3%) 20:26 (5%) ...	view
6	x 203	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems ...	lean S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_UnramQuad_free_f... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_FakeEllipticCur... S_CerednikDrinfeld_exists_disc_holOn_... S_CerednikDrinfeld_QM_FakeEllipticCur... S_CerednikDrinfeld_ringHom_functionFi... S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_FormalOmega_desc... ...	264:270 (1%) 12:18 (27%) 98:104 (1%) 532:538 (<1%) 132:138 (1%) 45:51 (1%) 81:87 (3%) 281:287 (1%) 56:62 (3%) 18:24 (5%) ...	view
6	x 199	P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol ...	lean S_AutomorphicForm_exists_isSemiLocalF... S_AutomorphicForm_normString_tensorAr... S_AutomorphicForm_mem_twistedStabiliz... S_AutomorphicForm_setIntegral_twisted... Thm_AutomorphicForm_exists_pos_forall... Thm_AutomorphicForm_lintegral_orbital... S_AutomorphicForm_integrableOn_convOp... S_AutomorphicForm_sum_lintegral_orbit... S_AutomorphicForm_setIntegral_central... S_AutomorphicForm_setIntegral_unipote... ...	1:6 (5%) 1:6 (8%) 1:6 (4%) 1:6 (1%) 1:6 (11%) 1:6 (7%) 1:6 (<1%) 1:6 (<1%) 1:6 (3%) 1:6 (4%) ...	view
6	x 199	P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems P2M/Sol P2M/Sol Theorems Theorems ...	lean S_AutomorphicForm_exists_isSemiLocalF... S_AutomorphicForm_normString_tensorAr... S_AutomorphicForm_integrableOn_convOp... S_AutomorphicForm_sum_lintegral_orbit... Thm_AutomorphicForm_exists_pos_forall... Thm_AutomorphicForm_lintegral_orbital... S_AutomorphicForm_setIntegral_central... S_AutomorphicForm_setIntegral_unipote... Thm_AutomorphicForm_exists_isSemiLoca... Thm_AutomorphicForm_mem_twistedStabil... ...	2:7 (5%) 2:7 (8%) 2:7 (<1%) 2:7 (<1%) 2:7 (11%) 2:7 (7%) 2:7 (3%) 2:7 (4%) 2:7 (10%) 2:7 (14%) ...	view
6	x 191	P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems P2M/Sol Theorems P2M/Sol ...	lean S_AutomorphicForm_exists_isSemiLocalF... S_AutomorphicForm_normString_tensorAr... S_AutomorphicForm_integrableOn_convOp... S_AutomorphicForm_sum_lintegral_orbit... S_AutomorphicForm_setIntegral_central... Thm_AutomorphicForm_exists_pos_forall... Thm_AutomorphicForm_lintegral_orbital... S_AutomorphicForm_setIntegral_unipote... Thm_AutomorphicForm_exists_isSemiLoca... S_AutomorphicForm_mem_twistedStabiliz... ...	5:10 (5%) 5:10 (8%) 5:10 (<1%) 5:10 (<1%) 5:10 (3%) 5:10 (11%) 5:10 (7%) 5:10 (4%) 5:10 (10%) 5:10 (4%) ...	view
6	x 188	P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems P2M/Sol Theorems P2M/Sol ...	lean S_AutomorphicForm_exists_isSemiLocalF... S_AutomorphicForm_normString_tensorAr... S_AutomorphicForm_integrableOn_convOp... S_AutomorphicForm_sum_lintegral_orbit... S_AutomorphicForm_setIntegral_central... Thm_AutomorphicForm_exists_pos_forall... Thm_AutomorphicForm_lintegral_orbital... S_AutomorphicForm_setIntegral_unipote... Thm_AutomorphicForm_exists_isSemiLoca... S_AutomorphicForm_mem_twistedStabiliz... ...	3:8 (5%) 3:8 (8%) 3:8 (<1%) 3:8 (<1%) 3:8 (3%) 3:8 (11%) 3:8 (7%) 3:8 (4%) 3:8 (10%) 3:8 (4%) ...	view
6	x 188	P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems P2M/Sol Theorems P2M/Sol ...	lean S_AutomorphicForm_exists_isSemiLocalF... S_AutomorphicForm_normString_tensorAr... S_AutomorphicForm_integrableOn_convOp... S_AutomorphicForm_sum_lintegral_orbit... S_AutomorphicForm_setIntegral_central... Thm_AutomorphicForm_exists_pos_forall... Thm_AutomorphicForm_lintegral_orbital... S_AutomorphicForm_setIntegral_unipote... Thm_AutomorphicForm_exists_isSemiLoca... S_AutomorphicForm_mem_twistedStabiliz... ...	4:9 (5%) 4:9 (8%) 4:9 (<1%) 4:9 (<1%) 4:9 (3%) 4:9 (11%) 4:9 (7%) 4:9 (4%) 4:9 (10%) 4:9 (4%) ...	view
6	x 164	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_CubicInduction_for... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_dual... S_LanglandsTunnell_RankinSelberg_dual... S_LanglandsTunnell_CubicInduction_exi... Thm_LanglandsTunnell_RankinSelberg_ex... ...	147:152 (1%) 63:68 (3%) 146:151 (1%) 68:73 (3%) 124:129 (2%) 1123:1128 (<1%) 805:810 (<1%) 122:127 (2%) 93:98 (3%) 63:68 (3%) ...	view
6	x 161	P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems P2M/Sol Theorems P2M/Sol P2M/Sol ...	lean S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_ringHom_functionFi... Thm_CerednikDrinfeld_FormalOmega_desc... Thm_CerednikDrinfeld_FormalOmega_desc... Thm_CerednikDrinfeld_QM_IsFineModuliT... S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_le_preimage_of_t... S_CerednikDrinfeld_FormalOmega_descen... S_CerednikDrinfeld_QM_IsFineModuli_ce... ...	104:109 (1%) 538:543 (<1%) 289:294 (1%) 25:30 (5%) 25:30 (6%) 44:49 (8%) 109:114 (1%) 24:29 (4%) 64:69 (2%) 28:33 (4%) ...	view
6	x 160	P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems P2M/Sol Theorems Theorems Theorems ...	lean S_AutomorphicForm_exists_isSemiLocalF... S_AutomorphicForm_normString_tensorAr... S_AutomorphicForm_integrableOn_convOp... S_AutomorphicForm_sum_lintegral_orbit... Thm_AutomorphicForm_exists_pos_forall... Thm_AutomorphicForm_lintegral_orbital... S_AutomorphicForm_forall_exists_lambd... Thm_AutomorphicForm_isInducedSection_... Thm_AutomorphicForm_TwistedBruhat_ae_... Thm_AutomorphicForm_forall_integral_s... ...	6:11 (5%) 6:11 (8%) 6:11 (<1%) 6:11 (<1%) 6:11 (11%) 6:11 (7%) 6:11 (<1%) 6:11 (6%) 6:11 (7%) 6:11 (12%) ...	view
6	x 160	P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems P2M/Sol Theorems Theorems Theorems ...	lean S_AutomorphicForm_exists_isSemiLocalF... S_AutomorphicForm_normString_tensorAr... S_AutomorphicForm_integrableOn_convOp... S_AutomorphicForm_sum_lintegral_orbit... Thm_AutomorphicForm_exists_pos_forall... Thm_AutomorphicForm_lintegral_orbital... S_AutomorphicForm_forall_exists_lambd... Thm_AutomorphicForm_isInducedSection_... Thm_AutomorphicForm_TwistedBruhat_ae_... Thm_AutomorphicForm_forall_integral_s... ...	7:12 (5%) 7:12 (8%) 7:12 (<1%) 7:12 (<1%) 7:12 (11%) 7:12 (7%) 7:12 (<1%) 7:12 (6%) 7:12 (7%) 7:12 (12%) ...	view
6	x 160	P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems P2M/Sol Theorems Theorems Theorems ...	lean S_AutomorphicForm_exists_isSemiLocalF... S_AutomorphicForm_normString_tensorAr... S_AutomorphicForm_integrableOn_convOp... S_AutomorphicForm_sum_lintegral_orbit... Thm_AutomorphicForm_exists_pos_forall... Thm_AutomorphicForm_lintegral_orbital... S_AutomorphicForm_forall_exists_lambd... Thm_AutomorphicForm_isInducedSection_... Thm_AutomorphicForm_TwistedBruhat_ae_... Thm_AutomorphicForm_forall_integral_s... ...	8:13 (5%) 8:13 (8%) 8:13 (<1%) 8:13 (<1%) 8:13 (11%) 8:13 (7%) 8:13 (<1%) 8:13 (6%) 8:13 (7%) 8:13 (12%) ...	view
6	x 157	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_dual... S_LanglandsTunnell_RankinSelberg_dual... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_CubicInduction_j... Thm_LanglandsTunnell_RankinSelberg_ex... ...	192:197 (1%) 108:113 (3%) 191:196 (1%) 113:118 (3%) 850:855 (<1%) 167:172 (2%) 109:114 (3%) 107:112 (4%) 55:60 (9%) 108:113 (4%) ...	view
6	x 157	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_dual... S_LanglandsTunnell_RankinSelberg_dual... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_CubicInduction_j... Thm_LanglandsTunnell_RankinSelberg_ex... ...	193:198 (1%) 109:114 (3%) 192:197 (1%) 114:119 (3%) 851:856 (<1%) 168:173 (2%) 110:115 (3%) 108:113 (4%) 56:61 (9%) 109:114 (4%) ...	view
6	x 157	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_dual... S_LanglandsTunnell_RankinSelberg_dual... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_CubicInduction_j... Thm_LanglandsTunnell_RankinSelberg_ex... ...	194:199 (1%) 110:115 (3%) 193:198 (1%) 115:120 (3%) 852:857 (<1%) 169:174 (2%) 111:116 (3%) 109:114 (4%) 57:62 (9%) 110:115 (4%) ...	view
6	x 156	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_dual... S_LanglandsTunnell_RankinSelberg_dual... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_CubicInduction_j... Thm_LanglandsTunnell_RankinSelberg_ex... ...	145:150 (1%) 61:66 (3%) 144:149 (1%) 66:71 (3%) 803:808 (<1%) 120:125 (2%) 62:67 (3%) 60:65 (4%) 46:51 (9%) 61:66 (4%) ...	view
6	x 156	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_dual... S_LanglandsTunnell_RankinSelberg_dual... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_CubicInduction_j... Thm_LanglandsTunnell_RankinSelberg_ex... ...	146:151 (1%) 62:67 (3%) 145:150 (1%) 67:72 (3%) 804:809 (<1%) 121:126 (2%) 63:68 (3%) 61:66 (4%) 47:52 (9%) 62:67 (4%) ...	view
6	x 155	P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems ...	lean S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_ringHom_functionFi... Thm_CerednikDrinfeld_FormalOmega_desc... S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_le_preimage_of_t... S_CerednikDrinfeld_FormalOmega_descen... S_CerednikDrinfeld_QM_IsFineModuli_ce... S_CerednikDrinfeld_FormalOmega_descen... Thm_CerednikDrinfeld_finite_affinoid_... ...	105:110 (1%) 539:544 (<1%) 290:295 (1%) 26:31 (5%) 110:115 (1%) 25:30 (4%) 65:70 (2%) 29:34 (4%) 25:30 (4%) 24:29 (6%) ...	view
6	x 155	P2M/Sol P2M/Sol P2M/Sol Theorems P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol Theorems ...	lean S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_QM_IsFineModuliT_e... S_CerednikDrinfeld_ringHom_functionFi... Thm_CerednikDrinfeld_FormalOmega_desc... S_CerednikDrinfeld_QM_FakeEllipticCur... Thm_CerednikDrinfeld_le_preimage_of_t... S_CerednikDrinfeld_FormalOmega_descen... S_CerednikDrinfeld_QM_IsFineModuli_ce... S_CerednikDrinfeld_FormalOmega_descen... Thm_CerednikDrinfeld_finite_affinoid_... ...	106:111 (1%) 540:545 (<1%) 291:296 (1%) 27:32 (5%) 111:116 (1%) 26:31 (4%) 66:71 (2%) 30:35 (4%) 26:31 (4%) 25:30 (6%) ...	view
6	x 151	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_dual... S_LanglandsTunnell_RankinSelberg_dual... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_CubicInduction_j... Thm_LanglandsTunnell_RankinSelberg_ex... ...	143:148 (1%) 59:64 (3%) 142:147 (1%) 64:69 (3%) 801:806 (<1%) 118:123 (2%) 60:65 (3%) 58:63 (4%) 44:49 (9%) 59:64 (4%) ...	view
6	x 151	P2M/Sol Theorems P2M/Sol P2M/Sol P2M/Sol P2M/Sol Theorems Theorems Theorems Theorems ...	lean S_LanglandsTunnell_RankinSelberg_exis... Thm_LanglandsTunnell_RankinSelberg_ex... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_exis... S_LanglandsTunnell_RankinSelberg_dual... S_LanglandsTunnell_RankinSelberg_dual... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_RankinSelberg_ex... Thm_LanglandsTunnell_CubicInduction_j... Thm_LanglandsTunnell_RankinSelberg_ex... ...	144:149 (1%) 60:65 (3%) 143:148 (1%) 65:70 (3%) 802:807 (<1%) 119:124 (2%) 61:66 (3%) 59:64 (4%) 45:50 (9%) 60:65 (4%) ...	view
6	x 148	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems Theorems P2M/Sol ...	lean S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_fin... Thm_ModularCurve_FullLevel_AuxLevel_c... S_ModularCurve_FullLevel_AuxLevel_blo... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_b... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_exi... ...	59:64 (1%) 50:55 (3%) 202:207 (1%) 51:56 (7%) 135:140 (1%) 52:57 (1%) 53:58 (2%) 50:55 (2%) 51:56 (1%) 52:57 (2%) ...	view
6	x 148	P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems P2M/Sol Theorems Theorems P2M/Sol ...	lean S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_fin... Thm_ModularCurve_FullLevel_AuxLevel_c... S_ModularCurve_FullLevel_AuxLevel_blo... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevelOne_... Thm_ModularCurve_FullLevel_AuxLevel_b... Thm_ModularCurve_FullLevel_AuxLevel_e... S_ModularCurve_FullLevel_AuxLevel_exi... ...	58:63 (1%) 49:54 (3%) 201:206 (1%) 50:55 (7%) 134:139 (1%) 51:56 (1%) 52:57 (2%) 49:54 (2%) 50:55 (1%) 51:56 (2%) ...	view

Duplicated Units

The list of top 23 duplicated units.

See data for all 23 unit duplicates...

Size	#	Folders	Files	Lines	Code
113	x 2	tools/docs-site/gen/assets html/assets	explorer.js explorer.js	40:164 40:164	view
136	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	4:155 4:155	view
38	x 2	tools/docs-site/gen/assets html/assets	hl.js hl.js	14:53 14:53	view
37	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	309:347 309:347	view
25	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	230:257 230:257	view
16	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	290:308 290:308	view
14	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	37:53 37:53	view
34	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	194:229 194:229	view
14	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	212:227 212:227	view
11	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	179:191 179:191	view
11	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	275:287 275:287	view
11	x 2	tools/docs-site/gen/assets html/assets	explorer.js explorer.js	6:18 6:18	view
51	x 2	tools/docs-site/gen/assets html/assets	hl.js hl.js	3:55 3:55	view
9	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	25:35 25:35	view
8	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	85:94 85:94	view
8	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	120:129 120:129	view
7	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	358:366 358:366	view
7	x 2	tools/docs-site/gen/assets html/assets	explorer.js explorer.js	52:60 52:60	view
6	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	384:391 384:391	view
6	x 2	tools/docs-site/gen/assets html/assets	explorer.js explorer.js	22:29 22:29	view
151	x 2	tools/docs-site/gen/assets html/assets	explorer.js explorer.js	2:165 2:165	view
18	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	209:228 209:228	view
11	x 2	tools/docs-site/gen/assets html/assets	site.js site.js	355:367 355:367	view

About This Analysis

For duplication, we look at places in code where there are 6 or more lines of code that are exactly the same.
Before duplication is calculated, the code is cleaned to remove empty lines, comments, and frequently duplicated constructs such as imports.
You should aim at having as little as possible (<5%) of duplicated code as high-level of duplication can lead to maintenance difficulties, poor factoring, and logical contradictions.

Learn more...

To learn more about duplications and techniques for eliminating duplication, Sokrates recommends the following resources:

Avoid Repetition, MartinFlower.com (IEEE Software article)
Refactoring duplicated code, sourcemaking.com
Beck Design Rules, MartinFowler.com
DRY (Don't Repeat Yourself) Principle, Wikipedia
The Cut-and-Paste Programming Software Development Anti-Pattern, sourcemaking.com
Code Smells / Duplicated Code, Jeff Atwood, codinghorror.com:

"Duplicated code is the bane of software development. Stamp out duplication whenever possible. You should always be on the lookout for more subtle cases of near-duplication, too. Don't Repeat Yourself!"

Reducing Coupling, MartinFlower.com (IEEE Software article):

"There are several ways to describe coupling, but it boils down to this: If changing one module in a program requires changing another module, then coupling exists. ... Duplication always implies coupling, because changing one piece of duplicate code implies changing the other."