# Iter-3 Bulk Import Log

Pre-integration : 5822 nodes, 9821 edges
Post-integration: 6225 nodes, 10351 edges

Chains processed     : 1595
Created theorem nodes: 92
Created state nodes  : 202
Created axiom nodes  : 109
Created edges        : 530
Skipped (already had edges): 1497
Unknown techniques   : 0

## Per-area

| Area | Chains parsed | Integrated | Skipped dup | Unknown tech |
|---|---|---|---|---|
| AL | 133 | 0 | 133 | 0 |
| AN2 | 66 | 1 | 65 | 0 |
| AN | 193 | 63 | 130 | 0 |
| CO | 81 | 0 | 81 | 0 |
| CS | 68 | 0 | 68 | 0 |
| DS | 112 | 0 | 112 | 0 |
| FA | 121 | 0 | 121 | 0 |
| GE | 109 | 30 | 79 | 0 |
| LO | 85 | 2 | 83 | 0 |
| MP | 70 | 0 | 70 | 0 |
| NT | 146 | 1 | 145 | 0 |
| PD | 137 | 1 | 136 | 0 |
| PR | 118 | 0 | 118 | 0 |
| TO | 156 | 0 | 156 | 0 |

## Skipped duplicate theorems (already wired)

- [AL] `s_cauchy_theorem` (Cauchy's theorem)
- [AL] `s_class_equation` (Class equation)
- [AL] `s_lagrange_theorem` (Lagrange's theorem)
- [AL] `s_orbit_stabilizer_theorem` (Orbit-stabilizer theorem)
- [AL] `s_burnside_counting_lemma` (Burnside's lemma)
- [AL] `s_burnside_paqb_solvable` (Burnside's p^a q^b solvability theorem)
- [AL] `s_feit_thompson_theorem` (Feit–Thompson odd-order theorem)
- [AL] `s_jordan_holder_theorem` (Jordan–Hölder theorem)
- [AL] `s_schreier_refinement_theorem` (Schreier refinement theorem)
- [AL] `s_krull_schmidt_theorem` (Krull–Schmidt theorem)
- [AL] `s_fundamental_theorem_fg_abelian` (Fundamental theorem of finitely generated abelian groups)
- [AL] `s_pid_structure_theorem` (Structure theorem for f.g. modules over a PID)
- [AL] `s_smith_normal_form_theorem` (Smith normal form)
- [AL] `s_cayley_theorem` (Cayley's theorem)
- [AL] `s_nielsen_schreier_theorem` (Nielsen–Schreier theorem)
- [AL] `s_kurosh_subgroup_theorem` (Kurosh subgroup theorem)
- [AL] `s_grushko_decomposition_theorem` (Grushko decomposition theorem)
- [AL] `s_stallings_ends_theorem` (Stallings theorem on ends of groups)
- [AL] `s_gromov_polynomial_growth_theorem` (Gromov's theorem on groups of polynomial growth)
- [AL] `s_tits_alternative_theorem` (Tits alternative)
- [AL] `s_fitting_theorem` (Fitting's theorem)
- [AL] `s_schur_zassenhaus_theorem` (Schur–Zassenhaus theorem)
- [AL] `s_frattini_argument` (Frattini's argument)
- [AL] `s_first_isomorphism_theorem` (Fundamental theorem on homomorphisms / first isomorphism theorem)
- [AL] `s_second_isomorphism_theorem` (Second isomorphism theorem (diamond))
- [AL] `s_third_isomorphism_theorem` (Third isomorphism theorem)
- [AL] `s_correspondence_theorem` (Correspondence theorem (lattice isomorphism))
- [AL] `s_maschke_theorem` (Maschke's theorem)
- [AL] `s_schurs_lemma` (Schur's lemma)
- [AL] `s_wedderburn_artin_theorem` (Wedderburn–Artin theorem)
- [AL] `s_jacobson_density_theorem` (Jacobson density theorem)
- [AL] `s_double_centralizer_theorem` (Double centralizer theorem)
- [AL] `s_skolem_noether_theorem` (Skolem–Noether theorem)
- [AL] `s_wedderburn_little_theorem` (Wedderburn's little theorem)
- [AL] `s_brauer_group_theorem` (Brauer group periodicity)
- [AL] `s_hilbert_90_theorem` (Hilbert's theorem 90)
- [AL] `s_artin_schreier_theorem` (Artin–Schreier theorem (characteristic p extensions))
- [AL] `s_kummer_theory_theorem` (Kummer theory)
- [AL] `s_luroth_theorem` (Lüroth's theorem)
- [AL] `s_primitive_element_theorem` (Primitive element theorem)
- [AL] `s_isomorphism_extension_theorem` (Isomorphism extension theorem)
- [AL] `s_steinitz_algebraic_closure_theorem` (Steinitz's theorem on field extensions)
- [AL] `s_frobenius_reciprocity_theorem` (Frobenius reciprocity)
- [AL] `s_mackey_decomposition_theorem` (Mackey decomposition / double coset formula)
- [AL] `s_character_orthogonality_theorem` (Character orthogonality relations)
- [AL] `s_burnside_character_vanish_theorem` (Burnside's theorem on character vanishing (zeros in character table))
- [AL] `s_brauer_induced_character_theorem` (Brauer's theorem on induced characters)
- [AL] `s_artin_induction_theorem` (Artin's induction theorem)
- [AL] `s_peter_weyl_theorem` (Peter–Weyl theorem)
- [AL] `s_weyl_complete_reducibility_theorem` (Weyl's theorem on complete reducibility)
- … and 1447 more