Theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups

(*
    File:     Finitely_Generated_Abelian_Groups.thy
    Author:   Joseph Thommes, TU München
*)
section ‹Fundamental Theorem of Finitely Generated Abelian Groups›

theory Finitely_Generated_Abelian_Groups
  imports DirProds Group_Relations
begin

notation integer_mod_group ("Z")

locale fin_gen_comm_group = comm_group +
  fixes gen :: "'a set"
  assumes gens_closed: "gen  carrier G"
  and     fin_gen: "finite gen"
  and     generators: "carrier G = generate G gen"

text ‹Every finite abelian group is also finitely generated.›

sublocale finite_comm_group  fin_gen_comm_group G "carrier G"
  using generate_incl generate_sincl by (unfold_locales, auto)

text ‹This lemma contains the proof of Kemper from his lecture notes on algebra~cite"kemper".
However, the proof is not done in the context of a finitely generated group but for a finitely
generated subgroup in a commutative group.›

lemma (in comm_group) ex_idirgen:
  fixes A :: "'a set"
  assumes "finite A" "A  carrier G"
  shows "gs. set gs  generate G A  distinct gs  is_idirprod (generate G A) (λg. generate G {g}) (set gs)
             successively (dvd) (map ord gs)  card (set gs)  card A"
  (is "?t A")
  using assms
proof (induction "card A" arbitrary: A rule: nat_less_induct)
  case i: 1
  show ?case
  proof (cases "relations A = {restrict (λ_. 0::int) A}") (* only trivial relation *)
    case True
    have fi: "finite A" by fact
    then obtain gs where gs: "set gs = A" "distinct gs" by (meson finite_distinct_list)
    have o: "ord g = 0" if "g  set gs" for g
      by (intro relations_zero_imp_ord_zero[OF that], use i(3) that True gs in auto)
    have m: "map ord gs = replicate (length gs) 0" using o
      by (induction gs; auto)
    show ?thesis
    proof(rule, safe)
      show "x. x  set gs  x  generate G A" using gs generate.incl[of _ A G] by blast
      show "distinct gs" by fact
      show "is_idirprod (generate G A) (λg. generate G {g}) (set gs)"
      proof(unfold is_idirprod_def, intro conjI, rule)
        show "generate G {g}  G" if "g  set gs" for g
          by (intro subgroup_imp_normal, use that generate_is_subgroup i(3) gs in auto)
        show "generate G A = IDirProds G (λg. generate G {g}) (set gs)" unfolding IDirProds_def
          by (subst gs(1), use generate_idem_Un i(3) in blast)
        show "compl_fam (λg. generate G {g}) (set gs)" using compl_fam_iff_relations_triv[OF i(2, 3)] o gs(1) True
          by blast
      qed
      show "successively (dvd) (map ord gs)" using m
      proof (induction gs)
        case c: (Cons a gs)
        thus ?case by(cases gs; simp)
      qed simp
      show "card (set gs)  card A" using gs by blast
    qed
  next
    case ntrel: False
    then have Ane: "A  {}"
      using i(2) triv_rel[of A] unfolding relations_def extensional_def by fastforce
    from ntrel obtain a where a: "a  A" "r relations A. r a  0" using i(2) triv_rel[of A]
      unfolding relations_def extensional_def by fastforce
    hence ac: "a  carrier G" using i(3) by blast
    have iH: "B.card B < card A; finite B; B  carrier G  ?t B"
      using i(1) by blast
    have iH2: "B. ?t B; generate G A = generate G B; card B < card A  ?t A"
      by fastforce
    show ?thesis
    proof(cases "inv a  (A - {a})")
      case True
      have "generate G A = generate G (A - {a})"
      proof(intro generate_subset_eqI[OF i(3)])
        show "A - (A - {a})  generate G (A - {a})"
        proof -
          have "A - (A - {a}) = {a}" using a True by auto
          also have "  generate G {inv a}" using generate.inv[of "inv a" "{inv a}" G] ac by simp
          also have "  generate G (A - {a})" by (intro mono_generate, use True in simp)
          finally show ?thesis .
        qed
      qed simp
      moreover have "?t (A - {a})"
        by (intro iH[of "A - {a}"], use i(2, 3) a(1) in auto, meson Ane card_gt_0_iff diff_Suc_less)
      ultimately show ?thesis using card.remove[OF i(2) a(1)] by fastforce
    next
      case inv: False
      define n where n: "n = card A"
      define all_gens where
        "all_gens = {gsPow (generate G A). finite gs  card gs  n  generate G gs = generate G A}"

      define exps where "exps = (gs'all_gens. relrelations gs'. nat ` {erel`gs'. e > 0})"
      define min_exp where "min_exp = Inf exps"

      have "exps  {}"
      proof -
        let ?B = "A - {a}  {inv a}"
        have "A  all_gens" unfolding all_gens_def using generate.incl n i(2) by fast
        moreover have "?B  all_gens"
        proof -
          have "card (A - {a}) = n - 1" using a n by (meson card_Diff_singleton_if i(2))
          hence "card ?B = n" using inv i(2, 3) n a(1)
            by (metis Un_empty_right Un_insert_right card.remove card_insert_disjoint finite_Diff)
          moreover have "generate G A = generate G ?B"
          proof(intro generate_one_switched_eqI[OF i(3) a(1), of _ "inv a"])
            show "inv a  generate G A" using generate.inv[OF a(1), of G] .
            show "a  generate G ?B"
            proof -
              have "a  generate G {inv a}" using generate.inv[of "inv a" "{inv a}" G] ac by simp
              also have "  generate G ?B" by (intro mono_generate, blast)
              finally show ?thesis .
            qed
          qed simp
          moreover hence "?B  generate G A" using generate_sincl by simp
          ultimately show ?thesis unfolding all_gens_def using i(2) by blast
        qed
        moreover have "(r  relations A. r a > 0)  (r  relations ?B. r (inv a) > 0)"
        proof(cases "r  relations A. r a > 0")
          case True
          then show ?thesis by blast
        next
          case False
          with a obtain r where r: "r  relations A" "r a < 0" by force
          have rc: "(λx. x [^] r x)  A  carrier G" using i(3) int_pow_closed by fast
          let ?r = "restrict (r(inv a := - r a)) ?B"
          have "?r  relations ?B"
          proof
            have "finprod G (λx. x [^] ?r x) ?B = finprod G (λx. x [^] r x) A"
            proof -
              have "finprod G (λx. x [^] ?r x) ?B
                  = finprod G (λx. x [^] ?r x) (insert (inv a) (A - {a}))" by simp
              also have " = (inv a) [^] ?r (inv a)  finprod G (λx. x [^] ?r x) (A - {a})"
              proof(intro finprod_insert[OF _ inv])
                show "finite (A - {a})" using i(2) by fast
                show "inv a [^] ?r (inv a)  carrier G"
                  using int_pow_closed[OF inv_closed[OF ac]] by fast
                show "(λx. x [^] ?r x)  A - {a}  carrier G" using int_pow_closed i(3) by fast
              qed
              also have " = a [^] r a  finprod G (λx. x [^] r x) (A - {a})"
              proof -
                have "(inv a) [^] ?r (inv a) = a [^] r a"
                  by (simp add: int_pow_inv int_pow_neg ac)
                moreover have "finprod G (λx. x [^] r x) (A - {a})
                             = finprod G (λx. x [^] ?r x) (A - {a})"
                proof(intro finprod_cong)
                  show "((λx. x [^] r x)  A - {a}  carrier G) = True" using rc by blast
                  have "i [^] r i = i [^] ?r i" if "i  A - {a}" for i using that inv by auto
                  thus "i. i  A - {a} =simp=> i [^] r i = i [^] restrict (r(inv a := - r a)) (A - {a}  {inv a}) i"
                    by algebra
                qed simp
                ultimately show ?thesis by argo
              qed
              also have " = finprod G (λx. x [^] r x) A"
                by (intro finprod_minus[symmetric, OF a(1) rc i(2)])
              finally show ?thesis .
            qed
            also have " = 𝟭" using r unfolding relations_def by fast
            finally show "finprod G (λx. x [^] ?r x) ?B = 𝟭" .
          qed simp
          then show ?thesis using r by fastforce
        qed
        ultimately show ?thesis unfolding exps_def using a by blast
      qed
      hence me: "min_exp  exps"
        unfolding min_exp_def using Inf_nat_def1 by force
      from cInf_lower min_exp_def have le: "x. x  exps  min_exp  x" by blast
      from me obtain gs rel g
        where gr: "gs  all_gens" "rel  relations gs" "g  gs" "rel g = min_exp" "min_exp > 0"
        unfolding exps_def by auto
      from gr(1) have cgs: "card gs  card A" unfolding all_gens_def n by blast
      with gr(3) have cgsg: "card (gs - {g}) < card A"
        by (metis Ane card.infinite card_Diff1_less card_gt_0_iff finite.emptyI
                  finite.insertI finite_Diff2 i.prems(1) le_neq_implies_less less_trans)
      from gr(1) have fgs: "finite gs" and gsg: "generate G gs = generate G A"
        unfolding all_gens_def n using i(2) card.infinite Ane by force+
      from gsg have gsc: "gs  carrier G" unfolding all_gens_def
        using generate_incl[OF i(3)] generate_sincl[of gs] by simp
      hence gc: "g  carrier G" using gr(3) by blast
      have ihgsg: "?t (gs - {g})"
        by (intro iH, use cgs fgs gsc gr(3) cgsg in auto)
      then obtain hs where
        hs: "set hs  generate G (gs - {g})" "distinct hs"
            "is_idirprod (generate G (gs - {g})) (λg. generate G {g}) (set hs)"
            "successively (dvd) (map ord hs)" "card (set hs)  card (gs - {g})" by blast
      hence hsc: "set hs  carrier G"
        using generate_sincl[of "set hs"] generate_incl[of "gs - {g}"] gsc by blast
      from hs(3) have ghs: "generate G (gs - {g}) = generate G (set hs)"
        unfolding is_idirprod_def IDirProds_def using generate_idem_Un[OF hsc] by argo
      have dvot: "?t A  (erel`gs. rel g dvd e)"
      proof(intro disjCI)
        assume na: "¬ (erel ` gs. rel g dvd e)"
        have "x. x  gs; ¬rel g dvd rel x  ?t A"
        proof -
          fix x
          assume x: "x  gs" "¬ rel g dvd rel x"
          hence xng: "x  g" by auto
          from x have xc: "x  carrier G" using gsc by blast
          have rg: "rel g > 0" using gr by simp
          define r::int where r: "r = rel x mod rel g"
          define q::int where q: "q = rel x div rel g"
          from r rg x have "r > 0"
            using mod_int_pos_iff[of "rel x" "rel g"] mod_eq_0_iff_dvd by force
          moreover have "r < rel g" using r rg by simp
          moreover have "rel x = q * rel g + r" using r q by presburger
          ultimately have rq: "rel x = q * (rel g) + r" "0 < r" "r < rel g" by auto
          define t where t: "t = g  x [^] q"
          hence tc: "t  carrier G" using gsc gr(3) x by fast
          define s where s: "s = gs - {g}  {t}"
          hence fs: "finite s" using fgs by blast
          have sc: "s  carrier G" using s tc gsc by blast
          have g: "generate G gs = generate G s"
          proof(unfold s, intro generate_one_switched_eqI[OF gsc gr(3), of _ t])
            show "t  generate G gs"
            proof(unfold t, intro generate.eng)
              show "g  generate G gs" using gr(3) generate.incl by fast
              show "x [^] q  generate G gs"
                using x generate_pow[OF xc] generate_sincl[of "{x}"] mono_generate[of "{x}" gs]
                by fast
            qed
            show "g  generate G (gs - {g}  {t})"
            proof -
              have gti: "g = t  inv (x [^] q)"
                using inv_solve_right[OF gc tc int_pow_closed[OF xc, of q]] t by blast
              moreover have "t  generate G (gs - {g}  {t})" by (intro generate.incl[of t], simp)
              moreover have "inv (x [^] q)  generate G (gs - {g})"
              proof -
                have "x [^] q  generate G {x}" using generate_pow[OF xc] by blast
                from generate_m_inv_closed[OF _ this] xc
                have "inv (x [^] q)  generate G {x}" by blast
                moreover have "generate G {x}  generate G (gs - {g})"
                  by (intro mono_generate, use x a in force)
                finally show ?thesis .
              qed
              ultimately show ?thesis
                using generate.eng mono_generate[of "gs - {g}" "gs - {g}  {t}"] by fast
            qed
          qed simp
          show "x  gs; ¬ rel g dvd rel x  ?t A"
          proof (cases "t  gs - {g}")
            case xt: True
            from xt have gts: "s = gs - {g}" using x s by auto
            moreover have "card (gs - {g}) < card gs" using fgs gr(3) by (meson card_Diff1_less)
            ultimately have "card (set hs) < card A" using hs(5) cgs by simp
            moreover have "set hs  generate G (set hs)" using generate_sincl by simp
            moreover have "distinct hs" by fact
            moreover have "is_idirprod (generate G (set hs)) (λg. generate G {g}) (set hs)"
              using hs ghs unfolding is_idirprod_def by blast
            moreover have "generate G A = generate G (set hs)" using g gts ghs gsg by argo
            moreover have "successively (dvd) (map ord hs)" by fact
            ultimately show "?t A" using iH2 by blast
          next
            case tngsg: False
            hence xnt: "x  t" using x xng by blast
            have "rel g dvd rel x"
            proof (rule ccontr)
              have "nat r  exps" unfolding exps_def
              proof
                show "s  all_gens" unfolding all_gens_def
                  using gsg g fgs generate_sincl[of s] switch_elem_card_le[OF gr(3), of t] cgs n s
                  by auto
                have xs: "x  s" using s xng x(1) by blast
                have ts: "t  s" using s by fast
                show "nat r  (relrelations s. nat ` {e  rel ` s. 0 < e})"
                proof
                  let ?r = "restrict (rel(x := r, t := rel g)) s"
                  show "?r  relations s"
                  proof
                    have "finprod G (λx. x [^] ?r x) s = finprod G (λx. x [^] rel x) gs"
                    proof -
                      have "finprod G (λx. x [^] ?r x) s = x [^] r  (t [^] rel g  finprod G (λx. x [^] rel x) (gs - {g} - {x}))"
                      proof -
                        have "finprod G (λx. x [^] ?r x) s = x [^] ?r x  finprod G (λx. x [^] ?r x) (s - {x})"
                          by (intro finprod_minus[OF xs _ fs], use sc in auto)
                        moreover have "finprod G (λx. x [^] ?r x) (s - {x}) = t [^] ?r t  finprod G (λx. x [^] ?r x) (s - {x} - {t})"
                          by (intro finprod_minus, use ts xnt fs sc in auto)
                        moreover have "finprod G (λx. x [^] ?r x) (s - {x} - {t}) = finprod G (λx. x [^] rel x) (s - {x} - {t})"
                          unfolding s by (intro finprod_cong',  use gsc in auto)
                        moreover have "s - {x} - {t} = gs - {g} - {x}" unfolding s using tngsg by blast
                        moreover hence "finprod G (λx. x [^] rel x) (s - {x} - {t}) = finprod G (λx. x [^] rel x) (gs - {g} - {x})" by simp
                        moreover have "x [^] ?r x = x [^] r" using xs xnt by auto
                        moreover have "t [^] ?r t = t [^] rel g" using ts by simp
                        ultimately show ?thesis by argo
                      qed
                      also have " = x [^] r  t [^] rel g  finprod G (λx. x [^] rel x) (gs - {g} - {x})"
                        by (intro m_assoc[symmetric], use xc tc in simp_all, intro finprod_closed, use gsc in fast)
                      also have " = g [^] rel g  x [^] rel x  finprod G (λx. x [^] rel x) (gs - {g} - {x})"
                      proof -
                        have "x [^] r  t [^] rel g = g [^] rel g  x [^] rel x"
                        proof -
                          have "x [^] r  t [^] rel g = x [^] r  (g  x [^] q) [^] rel g" using t by blast
                          also have " = x [^] r  x [^] (q * rel g)  g [^] rel g"
                          proof -
                            have "(g  x [^] q) [^] rel g = g [^] rel g  (x [^] q) [^] rel g"
                              using gc xc int_pow_distrib by auto
                            moreover have "(x [^] q) [^] rel g = x [^] (q * rel g)" using xc int_pow_pow by auto
                            moreover have "g [^] rel g  x [^] (q * rel g) = x [^] (q * rel g)  g [^] rel g"
                              using m_comm[OF int_pow_closed[OF xc] int_pow_closed[OF gc]] by simp
                            ultimately have "(g  x [^] q) [^] rel g = x [^] (q * rel g)  g [^] rel g" by argo
                            thus ?thesis by (simp add: gc m_assoc xc)
                          qed
                          also have " = x [^] rel x  g [^] rel g"
                          proof -
                            have "x [^] r  x [^] (q * rel g) = x [^] (q * rel g + r)"
                              by (simp add: add.commute int_pow_mult xc)
                            also have " = x [^] rel x" using rq by argo
                            finally show ?thesis by argo
                          qed
                          finally show ?thesis by (simp add: gc m_comm xc)
                        qed
                        thus ?thesis by simp
                      qed
                      also have " = g [^] rel g  (x [^] rel x  finprod G (λx. x [^] rel x) (gs - {g} - {x}))"
                        by (intro m_assoc, use xc gc in simp_all, intro finprod_closed, use gsc in fast)
                      also have " = g [^] rel g  finprod G (λx. x [^] rel x) (gs - {g})"
                      proof -
                        have "finprod G (λx. x [^] rel x) (gs - {g}) = x [^] rel x  finprod G (λx. x [^] rel x) (gs - {g} - {x})"
                          by (intro finprod_minus, use xng x(1) fgs gsc in auto)
                        thus ?thesis by argo
                      qed
                      also have " = finprod G (λx. x [^] rel x) gs" by (intro finprod_minus[symmetric, OF gr(3) _ fgs], use gsc in auto)
                      finally show ?thesis .
                    qed
                    thus "finprod G (λx. x [^] ?r x) s = 𝟭" using gr(2) unfolding relations_def by simp
                  qed auto
                  show "nat r  nat ` {e  ?r ` s. 0 < e}" using xs xnt rq(2) by fastforce
                qed
              qed
              from le[OF this] rq(3) gr(4, 5) show False by linarith
            qed
            thus "x  gs; ¬ rel g dvd rel x  ?t A" by blast
          qed
        qed
        thus "?t A" using na by blast
      qed
      show "?t A"
      proof (cases "erel`gs. rel g dvd e")
        case dv: True
        define tau where "tau = finprod G (λx. x [^] ((rel x) div rel g)) gs"
        have tc: "tau  carrier G"
          by (subst tau_def, intro finprod_closed[of "(λx. x [^] ((rel x) div rel g))" gs], use gsc in fast)
        have gts: "generate G gs = generate G (gs - {g}  {tau})"
        proof(intro generate_one_switched_eqI[OF gsc gr(3), of _ tau])
          show "tau  generate G gs" by (subst generate_eq_finprod_Pi_int_image[OF fgs gsc], unfold tau_def, fast)
          show "g  generate G (gs - {g}  {tau})"
          proof -
            have "tau = g  finprod G (λx. x [^] ((rel x) div rel g)) (gs - {g})"
            proof -
              have "finprod G (λx. x [^] ((rel x) div rel g)) gs = g [^] (rel g div rel g)  finprod G (λx. x [^] ((rel x) div rel g)) (gs - {g})"
                by (intro finprod_minus[OF gr(3) _ fgs], use gsc in fast)
              moreover have "g [^] (rel g div rel g) = g" using gr gsc by auto
              ultimately show ?thesis unfolding tau_def by argo
            qed
            hence gti: "g = tau  inv finprod G (λx. x [^] ((rel x) div rel g)) (gs - {g})"
              using inv_solve_right[OF gc tc finprod_closed[of "(λx. x [^] ((rel x) div rel g))" "gs - {g}"]] gsc
              by fast
            have "tau  generate G (gs - {g}  {tau})" by (intro generate.incl[of tau], simp)
            moreover have "inv finprod G (λx. x [^] ((rel x) div rel g)) (gs - {g})  generate G (gs - {g})"
            proof -
              have "finprod G (λx. x [^] ((rel x) div rel g)) (gs - {g})  generate G (gs - {g})"
                using generate_eq_finprod_Pi_int_image[of "gs - {g}"] fgs gsc by fast
              from  generate_m_inv_closed[OF _ this] gsc show ?thesis by blast
            qed
            ultimately show ?thesis by (subst gti, intro generate.eng, use mono_generate[of "gs - {g}"] in auto)
          qed
        qed simp
        with gr(1) have gt: "generate G (gs - {g}  {tau}) = generate G A" unfolding all_gens_def by blast
        have trgo: "tau [^] rel g = 𝟭"
        proof -
          have "tau [^] rel g = finprod G (λx. x [^] ((rel x) div rel g)) gs [^] rel g" unfolding tau_def by blast
          also have " = finprod G ((λx. x [^] rel g)  (λx. x [^] ((rel x) div rel g))) gs"
            by (intro finprod_exp, use gsc in auto)
          also have " = finprod G (λa. a [^] rel a) gs"
          proof(intro finprod_cong')
            show "((λx. x [^] rel g)  (λx. x [^] ((rel x) div rel g))) x = x [^] rel x" if "x  gs" for x
            proof -
              have "((λx. x [^] rel g)  (λx. x [^] ((rel x) div rel g))) x = x [^] (((rel x) div rel g) * rel g)"
                using that gsc int_pow_pow by auto
              also have " = x [^] rel x" using dv that by auto
              finally show ?thesis .
            qed
          qed (use gsc in auto)
          also have " = 𝟭" using gr(2) unfolding relations_def by blast
          finally show ?thesis .
        qed
        hence otdrg: "ord tau dvd rel g" using tc int_pow_eq_id by force
        have ot: "ord tau = rel g"
        proof -
          from gr(4, 5) have "rel g > 0" by simp
          with otdrg have "ord tau  rel g" by (meson zdvd_imp_le)
          moreover have "¬ord tau < rel g"
          proof
            assume a: "int (ord tau) < rel g"
            define T where T: "T = gs - {g}  {tau}"
            hence tT: "tau  T" by blast
            let ?r = "restrict ((λ_.(0::int))(tau := int(ord tau))) T"
            from T have "T  all_gens"
              using gt generate_sincl[of "gs - {g}  {tau}"] switch_elem_card_le[OF gr(3), of tau] fgs cgs n
              unfolding all_gens_def by auto
            moreover have "?r  relations T"
            proof(intro in_relationsI finprod_one_eqI)
              have "tau [^] int (ord tau) = 𝟭" using tc pow_ord_eq_1[OF tc] int_pow_int by metis
              thus "x [^] ?r x = 𝟭" if "x  T" for x using tT that by(cases "¬x = tau", auto)
            qed auto
            moreover have "?r tau = ord tau" using tT by auto
            moreover have "ord tau > 0" using dvd_nat_bounds gr(4) gr(5) int_dvd_int_iff otdrg by presburger
            ultimately have "ord tau  exps" unfolding exps_def using tT by (auto, force)
            with le a gr(4) show False by force
          qed
          ultimately show ?thesis by auto
        qed
        hence otnz: "ord tau  0" using gr me exps_def by linarith
        define l where l: "l = tau#hs"
        hence ls: "set l = set hs  {tau}" by auto
        with hsc tc have slc: "set l  carrier G" by auto
        have gAhst: "generate G A = generate G (set hs  {tau})"
        proof -
          have "generate G A = generate G (gs - {g}  {tau})" using gt by simp
          also have " = generate G (set hs  {tau})"
            by (rule generate_subset_change_eqI, use hsc gsc tc ghs in auto)
          finally show ?thesis .
        qed
        have glgA: "generate G (set l) = generate G A" using gAhst ls by simp
        have lgA: "set l  generate G A"
          using ls gt gts hs(1)
                mono_generate[of "gs - {g}" gs] generate.incl[of tau "gs - {g}  {tau}"]
          by fast
        show ?thesis
        proof (cases "ord tau = 1")
          case True
          hence "tau = 𝟭" using ord_eq_1 tc by blast
          hence "generate G A = generate G (gs - {g})"
            using gAhst generate_one_irrel hs(3) ghs by auto
          from iH2[OF ihgsg this cgsg] show ?thesis .
        next
          case otau: False
          consider (nd) "¬distinct l" | (ltn) "length l < n  distinct l" | (dn) "length l = n  distinct l"
          proof -
            have "length l  n"
            proof -
              have "length l = length hs + 1" using l by simp
              moreover have "length hs  card (gs - {g})" using hs(2, 5) by (metis distinct_card)
              moreover have "card (gs - {g}) + 1  n"
                using n cgsg gr(3) fgs Ane i(2) by (simp add: card_gt_0_iff)
              ultimately show ?thesis by linarith
            qed
            thus "¬ distinct l  thesis; length l < n  distinct l  thesis; length l = n  distinct l  thesis  thesis"
              by linarith
          qed
          thus ?thesis
          proof(cases)
            case nd
            with hs(2) l have ths: "set hs = set hs  {tau}" by auto
            hence "set l = set hs" using l by auto
            hence "generate G (gs - {g}) = generate G A" using gAhst ths ghs by argo
            moreover have "card (set hs)  card A"
              by (metis Diff_iff card_mono cgs dual_order.trans fgs hs(5) subsetI)
            ultimately show ?thesis using hs by auto
          next
            case ltn
            then have cl: "card (set l) < card A" using n by (metis distinct_card)
            from iH[OF this] hsc tc ls have "?t (set l)" by blast
            thus ?thesis by (subst (1 2) gAhst, use cl ls in fastforce)
          next
            case dn
            hence ln: "length l = n" and dl: "distinct l" by auto
            have c: "complementary (generate G {tau}) (generate G (gs - {g}))"
            proof -
              have "x = 𝟭" if "x  generate G {tau}  generate G (set hs)" for x
              proof -
                from that generate_incl[OF hsc] have xc: "x  carrier G" by blast
                from that have xgt: "x  generate G {tau}" and xgs: "x  generate G (set hs)"
                  by auto
                from generate_nat_pow[OF otnz tc] xgt have "a. a  0  a < ord tau  x = tau [^] a"
                  unfolding atLeastAtMost_def atLeast_def atMost_def
                  by (auto, metis Suc_pred less_Suc_eq_le neq0_conv otnz)
                then obtain a where a: "0  a" "a < ord tau" "x = tau [^] a" by blast
                then have ix: "inv x  generate G (set hs)"
                  using xgs generate_m_inv_closed ghs hsc by blast
                with generate_eq_finprod_Pi_int_image[OF _ hsc] obtain f where
                  f: "f  Pi (set hs) (λ_. (UNIV::int set))" "inv x = finprod G (λg. g [^] f g) (set hs)"
                  by blast
                let ?f = "restrict (f(tau := a)) (set l)"
                have fr: "?f  relations (set l)"
                proof(intro in_relationsI)
                  from ls dl l have sh: "set hs = set l - {tau}" by auto
                  have "finprod G (λa. a [^] ?f a) (set l) = tau [^] ?f tau  finprod G (λa. a [^] ?f a) (set hs)"
                    by (subst sh, intro finprod_minus, use l slc in auto)
                  moreover have "tau [^] ?f tau = x" using a l int_pow_int by fastforce
                  moreover have "finprod G (λa. a [^] ?f a) (set hs) = finprod G (λg. g [^] f g) (set hs)"
                    by (intro finprod_cong', use slc dl l in auto)
                  ultimately have "finprod G (λa. a [^] ?f a) (set l) = x  inv x" using f by argo
                  thus "finprod G (λa. a [^] ?f a) (set l) = 𝟭" using xc by auto
                qed blast
                have "¬a > 0"
                proof
                  assume ag: "0 < a"
                  have "set l  all_gens" unfolding all_gens_def using glgA lgA dn distinct_card
                    by fastforce
                  moreover have "int a = ?f tau" using l by auto
                  moreover have "tau  set l" using l by simp
                  ultimately have "a  exps" using fr ag unfolding exps_def by (auto, force)
                  from le[OF this] a(2) ot gr(4) show False by simp
                qed
                hence "a = 0" using a by blast
                thus "x = 𝟭" using tc a by force
              qed
              thus ?thesis unfolding complementary_def using generate.one ghs by blast
            qed
            moreover have idl: "is_idirprod (generate G A) (λg. generate G {g}) (set l)"
            proof -
              have "is_idirprod (generate G (set hs  {tau})) (λg. generate G {g}) (set hs  {tau})"
                by (intro idirprod_generate_ind, use tc hsc hs(3) ghs c in auto)
              thus ?thesis using ls gAhst by auto
            qed
            moreover have "¬?t A  successively (dvd) (map ord l)"
            proof (cases hs)
              case Nil
              thus ?thesis using l by simp
            next
              case (Cons a list)
              hence ac: "a  carrier G" using hsc by auto
              assume nA: "¬?t A"
              have "ord tau dvd ord a"
              proof (rule ccontr)
                assume nd: "¬ ord tau dvd ord a"
                then have 0 < ord a mod ord tau
                  using mod_eq_0_iff_dvd by auto
                have "int (ord tau) > 0" using otnz by simp
                obtain r q :: int where rq: "ord a = q * (ord tau) + r" "0 < r" "r < ord tau"
                  by (rule that [of ord a div ord tau ord a mod ord tau])
                    (use otnz 0 < ord a mod ord tau in simp_all add: div_mult_mod_eq flip: of_nat_mult of_nat_add)
                define b where b: "b = tau  a [^] q"
                hence bc: "b  carrier G" using hsc tc Cons by auto
                have g: "generate G (set (b#hs)) = generate G (set l)"
                proof -
                  have se: "set (b#hs) = set l - {tau}  {b}" using l Cons dl by auto
                  show ?thesis
                  proof(subst se, intro generate_one_switched_eqI[symmetric, of _ tau _ b])
                    show "b  generate G (set l)"
                    proof -
                      have "tau  generate G (set l)" using l generate.incl[of tau "set l"] by auto
                      moreover have "a [^] q  generate G (set l)"
                        using mono_generate[of "{a}" "set l"] generate_pow[OF ac] Cons l by auto
                      ultimately show ?thesis using b generate.eng by fast
                    qed
                    show "tau  generate G (set l - {tau}  {b})"
                    proof -
                      have "tau = b  inv(a [^] q)" by (simp add: ac b m_assoc tc)
                      moreover have "b  generate G (set l - {tau}  {b})"
                        using generate.incl[of b "set l - {tau}  {b}"] by blast
                      moreover have "inv(a [^] q)  generate G (set l - {tau}  {b})"
                      proof -
                        have "generate G {a}  generate G (set l - {tau}  {b})"
                          using mono_generate[of "{a}" "set l - {tau}  {b}"] dl Cons l by auto
                        moreover have "inv(a [^] q)  generate G {a}"
                          by (subst generate_pow[OF ac], subst int_pow_neg[OF ac, of q, symmetric], blast)
                        ultimately show ?thesis by fast
                      qed
                      ultimately show ?thesis using generate.eng by fast
                    qed
                  qed (use bc tc hsc dl Cons l in auto)
                qed
                show False
                proof (cases "card (set (b#hs))  n")
                  case True
                  hence cln: "card (set (b#hs)) < n"
                    using l Cons ln by (metis card_length list.size(4) nat_less_le)
                  hence seq: "set (b#hs) = set hs"
                  proof -
                    from dn l Cons True have "b  set hs"
                      by (metis distinct.simps(2) distinct_card list.size(4))
                    thus ?thesis by auto
                  qed
                  with cln have clA: "card (set hs) < card A" using n by auto
                  moreover have "set hs  generate G (set hs)" using generate_sincl by simp
                  moreover have "distinct hs" by fact
                  moreover have "is_idirprod (generate G (set hs)) (λg. generate G {g}) (set hs)"
                    by (intro is_idirprod_generate, use hs[unfolded is_idirprod_def] hsc in auto)
                  moreover have "generate G A = generate G (set hs)" using glgA g seq by argo
                  moreover have "successively (dvd) (map ord hs)" by fact
                  ultimately show False using iH2 nA by blast
                next
                  case False
                  hence anb: "a  b"
                    by (metis card_distinct distinct_length_2_or_more l list.size(4) ln local.Cons)
                  have "nat r  exps" unfolding exps_def
                  proof(rule)
                    show "set (b#hs)  all_gens" unfolding all_gens_def
                      using gAhst g ls generate_sincl[of "set (b#hs)"] False by simp
                    let ?r = "restrict ((λ_. 0::int)(b := ord tau, a := r)) (set (b#hs))"
                    have "?r  relations (set (b#hs))"
                    proof(intro in_relationsI)
                      show "finprod G (λx. x [^] ?r x) (set (b#hs)) = 𝟭"
                      proof -
                        have "finprod G (λx. x [^] ?r x) (set (b#hs)) = b [^] ?r b  finprod G (λx. x[^] ?r x) (set (b#hs) - {b})"
                          by (intro finprod_minus, use hsc Cons bc in auto)
                        moreover have "finprod G (λx. x[^] ?r x) (set (b#hs) - {b}) = a [^] ?r a  finprod G (λx. x[^] ?r x) (set (b#hs) - {b} - {a})"
                          by (intro finprod_minus, use hsc Cons False n anb in auto)
                        moreover have "finprod G (λx. x[^] ?r x) (set (b#hs) - {b} - {a}) = 𝟭"
                          by (intro finprod_one_eqI, simp)
                        ultimately have "finprod G (λx. x [^] ?r x) (set (b#hs)) = b [^] ?r b  (a [^] ?r a  𝟭)"
                          by argo
                        also have " = b [^] ?r b  a [^] ?r a" using Cons hsc by simp
                        also have " = b [^] int(ord tau)  a [^] r" using anb Cons by simp
                        also have " = 𝟭"
                        proof -
                          have "b [^] int (ord tau) = tau [^] int (ord tau)  (a [^] q) [^] int (ord tau)"
                            using b bc hsc int_pow_distrib local.Cons tc by force
                          also have " = (a [^] q) [^] int (ord tau)"
                            using trgo hsc local.Cons ot by force
                          finally have "b [^] int (ord tau)  a [^] r = (a [^] q) [^] int (ord tau)  a [^] r"
                            by argo
                          also have " = a [^] (q * int (ord tau) + r)" using Cons hsc
                            by (metis comm_group_axioms comm_group_def group.int_pow_pow
                                      int_pow_mult list.set_intros(1) subsetD)
                          also have " = a [^] int (ord a)" using rq by argo
                          finally show ?thesis using Cons hsc int_pow_eq_id by simp
                        qed
                        finally show ?thesis .
                      qed
                    qed simp
                    moreover have "r  {e  ?r ` set (b # hs). 0 < e}"
                    proof (rule, rule, rule)
                      show "0 < r" by fact
                      show "a  set (b#hs)" using Cons by simp
                      thus "r = ?r a" by auto
                    qed
                    ultimately show "nat r  (relrelations (set (b # hs)). nat ` {e  rel ` set (b # hs). 0 < e})"
                      by fast
                  qed
                  moreover have "nat r < min_exp" using ot rq(2, 3) gr(4) by linarith
                  ultimately show False using le by fastforce
                qed
              qed
              thus ?thesis using hs(4) Cons l by simp
            qed
            ultimately show ?thesis using lgA n dn by (metis card_length)
          qed
        qed
      qed (use dvot in blast)
    qed
  qed
qed

lemma (in comm_group) fundamental_subgr:
  fixes A :: "'a set"
  assumes "finite A" "A  carrier G"
  obtains gs where
    "set gs  generate G A" "distinct gs" "is_idirprod (generate G A) (λg. generate G {g}) (set gs)"
    "successively (dvd) (map ord gs)" "card (set gs)  card A"
  using assms ex_idirgen by meson

text ‹As every group is a subgroup of itself, the theorem follows directly. However, for reasons of
convenience and uniqueness (although not completely proved), we strengthen the result by proving
that the decomposition can be done without having the trivial factor in the product.
We formulate the theorem in various ways: firstly, the invariant factor decomposition.›

theorem (in fin_gen_comm_group) invariant_factor_decomposition_idirprod:
  obtains gs where
    "set gs  carrier G" "distinct gs" "is_idirprod (carrier G) (λg. generate G {g}) (set gs)"
    "successively (dvd) (map ord gs)" "card (set gs)  card gen" "𝟭  set gs"
proof -
  from fundamental_subgr[OF fin_gen gens_closed] obtain gs where
  gs: "set gs  carrier G" "distinct gs" "is_idirprod (carrier G) (λg. generate G {g}) (set gs)"
    "successively (dvd) (map ord gs)" "card (set gs)  card gen" using generators by auto
  hence cf: "compl_fam (λg. generate G {g}) (set gs)" by simp
  let ?r = "remove1 𝟭 gs"
  have r: "set ?r = set gs - {𝟭}" using gs by auto
  have "set ?r  carrier G" using gs by auto
  moreover have "distinct ?r" using gs by auto
  moreover have "is_idirprod (carrier G) (λg. generate G {g}) (set ?r)"
  proof (intro is_idirprod_generate)
    show "set ?r  carrier G" using gs by auto
    show "compl_fam (λg. generate G {g}) (set (remove1 𝟭 gs))"
      by (rule compl_fam_generate_subset[OF cf gs(1)], use set_remove1_subset in fastforce)
    show "carrier G = generate G (set ?r)"
    proof -
      have "generate G (set ?r) = generate G (set gs)" using generate_one_irrel' r by simp
      with gs(3) show ?thesis by simp
    qed
  qed
  moreover have "successively (dvd) (map ord ?r)"
  proof (cases gs)
    case (Cons a list)
    have r: "(map ord (remove1 𝟭 gs)) = remove1 1 (map ord gs)" using gs(1)
    proof(induction gs)
      case (Cons a gs)
      hence "a  carrier G" by simp
      with Cons ord_eq_1[OF this] show ?case by auto
    qed simp
    show ?thesis by (unfold r,
                     rule transp_successively_remove1[OF _ gs(4), unfolded transp_def],
                     auto)
  qed simp
  moreover have "card (set ?r)  card gen" using gs(5) r
    by (metis List.finite_set card_Diff1_le dual_order.trans)
  moreover have "𝟭  set ?r" using gs(2) by auto
  ultimately show ?thesis using that by blast
qed

corollary (in fin_gen_comm_group) invariant_factor_decomposition_dirprod:
  obtains gs where
    "set gs  carrier G" "distinct gs"
    "DirProds (λg. Gcarrier := generate G {g}) (set gs)  G"
    "successively (dvd) (map ord gs)" "card (set gs)  card gen"
    "compl_fam (λg. generate G {g}) (set gs)" "𝟭  set gs"
proof -
  from invariant_factor_decomposition_idirprod obtain gs where
    gs: "set gs  carrier G" "distinct gs" "is_idirprod (carrier G) (λg. generate G {g}) (set gs)"
        "successively (dvd) (map ord gs)" "card (set gs)  card gen" "𝟭  set gs" by blast
  with cong_DirProds_IDirProds[OF gs(3)] gs
  have "DirProds (λg. Gcarrier := generate G {g}) (set gs)  G" by blast
  with gs that show ?thesis by auto
qed

corollary (in fin_gen_comm_group) invariant_factor_decomposition_dirprod_fam:
  obtains Hs where
    "H. H  set Hs  subgroup H G" "distinct Hs"
    "DirProds (λH. Gcarrier := H) (set Hs)  G" "successively (dvd) (map card Hs)"
    "card (set Hs)  card gen" "compl_fam id (set Hs)" "{𝟭}  set Hs"
proof -
  from invariant_factor_decomposition_dirprod obtain gs where
  gs: "set gs  carrier G" "distinct gs"
      "DirProds (λg. Gcarrier := generate G {g}) (set gs)  G"
      "successively (dvd) (map ord gs)" "card (set gs)  card gen"
      "compl_fam (λg. generate G {g}) (set gs)" "𝟭  set gs" by blast
  let ?gen = "(λg. generate G {g})"
  let ?Hs = "map (λg. ?gen g) gs"
  have "subgroup H G" if "H  set ?Hs" for H using that gs by (auto intro: generate_is_subgroup)
  moreover have "distinct ?Hs"
    using compl_fam_imp_generate_inj[OF gs(1)] gs distinct_map by blast
  moreover have "DirProds (λH. Gcarrier := H) (set ?Hs)  G"
  proof -
    have gg: "group (Gcarrier := ?gen g)" if "g  set gs" for g
      by (use gs that in auto intro: subgroup.subgroup_is_group generate_is_subgroup)
    then interpret og: group "DirProds (λg. Gcarrier := ?gen g) (set gs)"
      using DirProds_group_iff by blast
    have "DirProds (λg. Gcarrier := ?gen g) (set gs)  DirProds (λH. Gcarrier := H) (set ?Hs)"
    proof (intro DirProds_iso[of ?gen])
      show "bij_betw ?gen (set gs) (set ?Hs)"
        using distinct ?Hs gs(2) compl_fam_imp_generate_inj[OF gs(1, 6)]
        by (simp add: bij_betw_def)
      show "Gcarrier := ?gen g  Gcarrier := ?gen g" if "g  set gs" for g by simp
      show "group (Gcarrier := ?gen g)" if "g  set gs" for g using that by fact
      show "Group.group (Gcarrier := H)" if "H  set ?Hs" for H
        by (use gs that in auto intro: subgroup.subgroup_is_group generate_is_subgroup)
    qed
    from group.iso_sym[OF og.is_group this] show ?thesis using gs iso_trans by blast
  qed
  moreover have "successively (dvd) (map card ?Hs)"
  proof -
    have "card (generate G {g}) = ord g" if "g  set gs" for g
      using generate_pow_card that gs(1) by auto
    hence "map card ?Hs = map ord gs" by simp
    thus ?thesis using gs(4) by argo
  qed
  moreover have "card (set ?Hs)  card gen" using gs
    by (metis distinct ?Hs distinct_card length_map)
  moreover have "compl_fam id (set ?Hs)"
    using compl_fam_cong[OF _ compl_fam_imp_generate_inj[OF gs(1, 6)], of id] using gs by auto
  moreover have "{𝟭}  set ?Hs" using generate_singleton_one gs by auto
  ultimately show ?thesis using that by blast
qed

text ‹Here, the invariant factor decomposition in its classical form.›

corollary (in fin_gen_comm_group) invariant_factor_decomposition_Zn:
  obtains ns where
    "DirProds (λn. Z (ns!n)) {..<length ns}  G" "successively (dvd) ns" "length ns  card gen"
proof -
  from invariant_factor_decomposition_dirprod obtain gs where
      gs: "set gs  carrier G" "distinct gs"
          "DirProds (λg. Gcarrier := generate G {g}) (set gs)  G"
          "successively (dvd) (map ord gs)" "card (set gs)  card gen"
          "compl_fam (λg. generate G {g}) (set gs)" "𝟭  set gs" by blast
  let ?DP = "DirProds (λg. Gcarrier := generate G {g}) (set gs)"
  have "ns. DirProds (λn. Z (ns!n)) {..<length ns}  G
            successively (dvd) ns  length ns  card gen"
  proof (cases gs, rule)
    case Nil
    from gs(3) Nil have co: "carrier ?DP = {𝟭?DP}" unfolding DirProds_def by auto
    let ?ns = "[]"
    have "DirProds (λn. Z ([] ! n)) {}  ?DP"
    proof(intro triv_iso DirProds_is_group)
      show "carrier (DirProds (λn. Z ([] ! n)) {}) = {𝟭DirProds (λn. Z ([] ! n)) {}}"
        using DirProds_empty by blast
    qed (use co group_integer_mod_group Nil in auto)
    from that[of ?ns] gs co iso_trans[OF this gs(3)]
    show "DirProds (λn. Z (?ns ! n)) {..<length ?ns}  G
         successively (dvd) ?ns  length ?ns  card gen"
      unfolding lessThan_def by simp
  next
    case c: (Cons a list)
    let ?l = "map ord gs"
    from c have l: "length ?l > 0" by auto
    have "DirProds (λn. Z (?l ! n)) {..<length ?l}  G"
    proof -
      have "DirProds (λn. Z (?l ! n)) {..<length ?l}  ?DP"
      proof(intro DirProds_iso[where ?f = "λn. gs!n"])
        show "bij_betw ((!) gs) {..<length ?l} (set gs)" using gs
          by (simp add: bij_betw_nth)
        show "Z (map ord gs ! i)  Gcarrier := generate G {gs ! i}" if "i  {..<length ?l}" for i
        proof(rule group.iso_sym[OF subgroup.subgroup_is_group[OF generate_is_subgroup]
                   cyclic_group.Zn_iso[OF cyclic_groupI2]])
          show "order (Gcarrier := generate G {gs ! i}) = map ord gs ! i"
            unfolding order_def using that generate_pow_card[of "gs ! i"] gs(1) by force
        qed (use gs(1) that in auto)
        show "Group.group (Z (map ord gs ! i))" if "i  {..<length (map ord gs)}" for i
          using group_integer_mod_group by blast
        show "Group.group (Gcarrier := generate G {g})" if "g  set gs" for g
          using that gs(1) subgroup.subgroup_is_group[OF generate_is_subgroup] by auto
      qed
      from iso_trans[OF this gs(3)] show ?thesis .
    qed
    moreover have "length ?l  card gen" using gs by (metis distinct_card length_map)
    ultimately show ?thesis using gs c by fastforce
  qed
  thus ?thesis using that by blast
qed

text ‹As every integer_mod_group› can be decomposed into a product of prime power groups,
we obtain (by using the fact that the direct product does not care about nestedness)
the primary decomposition.›

lemma Zn_iso_DirProds_prime_powers:
  assumes "n  0"
  shows "Z n  DirProds (λp. Z (p ^ multiplicity p n)) (prime_factors n)" (is "Z n  ?DP")
proof (cases "n = 1")
  case True
  show ?thesis by (intro triv_iso[OF group_integer_mod_group DirProds_is_group],
                   use DirProds_empty carrier_integer_mod_group True in auto)
next
  case nno: False
  interpret DP: group ?DP by (intro DirProds_is_group, use group_integer_mod_group in blast)
  have "order ?DP = prod (order  (λp. Z (p ^ multiplicity p n))) (prime_factors n)"
    by (intro DirProds_order, blast)
  also have " = prod (λp. p ^ multiplicity p n) (prime_factors n)" using Zn_order by simp
  also have n: " = n" using prod_prime_factors[OF assms] by simp
  finally have oDP: "order ?DP = n" .
  then interpret DP: finite_group ?DP
    by (unfold_locales, unfold order_def, metis assms card.infinite)
  let ?f = "λp(prime_factors n). 1"
  have fc: "?f  carrier ?DP"
  proof -
    have p: "0 < multiplicity p n" if "p  prime_factors n" for p
      using prime_factors_multiplicity that by auto
    have pk: "1 < p ^ k" if "Factorial_Ring.prime p" "0 < k" for p k::nat
      using that one_less_power prime_gt_1_nat by blast
    show ?thesis unfolding DirProds_def PiE_def
      by(use carrier_integer_mod_group assms nno pk p in auto,
         metis in_prime_factors_iff nat_int of_nat_power one_less_nat_eq)
  qed
  have of: "DP.ord ?f = n"
  proof -
    have "n dvd j" if j: "?f [^]?DPj = 𝟭?DP⇙" for j
    proof (intro pairwise_coprime_dvd'[OF _ _ n[symmetric]])
      show "finite (prime_factors n)" by simp
      show "a∈#prime_factorization n. a ^ multiplicity a n dvd j"
      proof
        show "p ^ multiplicity p n dvd j" if "p  prime_factors n" for p
        proof -
          from j have "(?f [^]?DPj) p = 0"
            using that unfolding DirProds_def one_integer_mod_group by auto
          hence "?f p [^]Z (p ^ multiplicity p n)j = 0" using comp_exp_nat[OF that] by metis
          hence "group.ord (Z (p ^ multiplicity p n)) (?f p) dvd j" using comp_in_carr[OF fc that]
            by (metis group.pow_eq_id group_integer_mod_group one_integer_mod_group)
          moreover have "group.ord (Z (p ^ multiplicity p n)) (?f p) = p ^ multiplicity p n"
            by (metis (no_types, lifting) Zn_neq1_cyclic_group Zn_order comp_in_carr
                                          cyclic_group.ord_gen_is_group_order fc integer_mod_group_1
                                          restrict_apply' that)
          ultimately show ?thesis by simp
        qed
      qed
      show "coprime (i ^ multiplicity i n) (j ^ multiplicity j n)"
        if "i ∈# prime_factorization n" "j ∈# prime_factorization n" "i  j" for i j
        using that diff_prime_power_imp_coprime by blast
    qed
    thus ?thesis using fc DP.ord_dvd_group_order gcd_nat.asym oDP by force
  qed
  interpret DP: cyclic_group ?DP ?f by (intro DP.element_ord_generates_cyclic, use of oDP fc in auto)
  show ?thesis using DP.iso_sym[OF DP.Zn_iso[OF oDP]] .
qed

lemma Zn_iso_DirProds_prime_powers':
  assumes "n  0"
  shows "Z n  DirProds (λp. Z p) ((λp. p ^ multiplicity p n) ` (prime_factors n))" (is "Z n  ?DP")
proof -
  have cp: "(λp. Z (p ^ multiplicity p n)) = (λp. Z p)  (λp. p ^ multiplicity p n)" by auto
  have "DirProds (λp. Z (p ^ multiplicity p n)) (prime_factors n)  ?DP"
  proof(subst cp, intro DirProds_iso2)
    show "inj_on (λp. p ^ multiplicity p n) (prime_factors n)"
      by (intro inj_onI; simp add: prime_factors_multiplicity prime_power_inj'')
    show "group (DirProds Z ((λp. p ^ multiplicity p n) ` prime_factors n))"
      by (intro DirProds_is_group, use group_integer_mod_group in auto)
  qed
  with Zn_iso_DirProds_prime_powers[OF assms] show ?thesis using Group.iso_trans by blast
qed

corollary (in fin_gen_comm_group) primary_decomposition_Zn:
  obtains ns where
    "DirProds (λn. Z (ns!n)) {..<length ns}  G"
    "nset ns. n = 0  (p k. Factorial_Ring.prime p  k > 0  n = p ^ k)"
proof -
  from invariant_factor_decomposition_Zn obtain ms where
    ms: "DirProds (λm. Z (ms!m)) {..<length ms}  G" "successively (dvd) ms" "length ms  card gen"
    by blast
  let ?I = "{..<length ms}"
  let ?J = "λi. if ms!i = 0 then {0} else (λp. p ^ multiplicity p (ms!i)) ` (prime_factors (ms!i))"
  let ?G = "λi. Z"
  let ?f = "λi. DirProds (?G i) (?J i)"
  have "DirProds (λm. Z (ms!m)) {..<length ms}  DirProds ?f {..<length ms}"
  proof (intro DirProds_iso[of id])
    show "bij_betw id {..<length ms} {..<length ms}" by blast
    show "Z (ms ! i)  ?f (id i)" if "i  {..<length ms}" for i
      by (cases "ms!i = 0",
          simp add: DirProds_one_cong_sym,
          auto intro: Zn_iso_DirProds_prime_powers')
    show "i. i  {..<length ms}  group (Z (ms ! i))" by auto
    show "group (?f j)" if "j  {..<length ms}" for j by (auto intro: DirProds_is_group)
  qed
  also have "  DirProds (λ(i,j). ?G i j) (Sigma ?I ?J)"
    by(rule DirProds_Sigma)
  finally have G1: "G  DirProds (λ(i,j). ?G i j) (Sigma ?I ?J)" using ms(1)
    by (metis (no_types, lifting) DirProds_is_group Group.iso_trans group.iso_sym group_integer_mod_group)
  have "ps. set ps = Sigma ?I ?J  distinct ps" by(intro finite_distinct_list, auto)
  then obtain ps where ps: "set ps = Sigma ?I ?J" "distinct ps" by blast
  define ns where ns: "ns = map snd ps"
  have "DirProds (λn. Z (ns!n)) {..<length ns}  DirProds (λ(i,j). ?G i j) (Sigma ?I ?J)"
  proof -
    obtain b::"nat  (nat × nat)"
      where b: "i<length ns. ns!i = snd (b i)" "bij_betw b {..<length ns} (Sigma ?I ?J)"
      using ns ps bij_betw_nth by fastforce
    moreover have "Z (ns ! i)  (case b i of (i, x)  Z x)" if "i  {..<length ns}" for i
    proof -
      have "ns ! i = snd (b i)" using b that by blast
      thus ?thesis by (simp add: case_prod_beta)
    qed
    ultimately show ?thesis by (auto intro: DirProds_iso)
  qed
  with G1 have "DirProds (λn. Z (ns!n)) {..<length ns}  G" using Group.iso_trans iso_sym by blast
  moreover have "n = 0  (p k. Factorial_Ring.prime p  k > 0  n = p ^ k)" if "nset ns" for n
  proof -
    have "k = 0  (pprime_factors (ms!i). k = p ^ multiplicity p (ms!i))" if "k  ?J i" for k i
      by (cases "ms!i = 0", use that in auto)
    with that ns ps show ?thesis
      by (auto, metis (no_types, lifting) mem_Collect_eq neq0_conv prime_factors_multiplicity)
  qed
  ultimately show
  "(ns. DirProds (λn. Z (ns ! n)) {..<length ns}  G;
          nset ns. n = 0  (p k. Factorial_Ring.prime p  k > 0  n = p ^ k)  thesis)
     thesis" by blast
qed

text ‹As every finite group is also finitely generated, it follows that a finite group can be
decomposed in a product of finite cyclic groups.›

lemma (in finite_comm_group) cyclic_product:
  obtains ns where "DirProds (λn. Z (ns!n)) {..<length ns}  G" "nset ns. n0"
proof -
  from primary_decomposition_Zn obtain ns where
    ns: "DirProds (λn. Z (ns ! n)) {..<length ns}  G"
        "nset ns. n = 0  (p k. normalization_semidom_class.prime p  0 < k  n = p ^ k)"
    by blast
  have "False" if "n  {..<length ns}" "ns!n = 0" for n
  proof -
    from that have "order (DirProds (λn. Z (ns ! n)) {..<length ns}) = 0"
      using DirProds_order[of "{..<length ns}" "λn. Z (ns!n)"] Zn_order by auto
    with fin iso_same_card[OF ns(1)] show False unfolding order_def by auto
  qed
  hence "nset ns. n0"
    by (metis in_set_conv_nth lessThan_iff)
  with ns show ?thesis using that by blast
qed

no_notation integer_mod_group ("Z")

end