Theory group

⊢ ∀g. AbelianGroup g ⇔ Group g ∧ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x

⊢ ∀g h. CosetPartition g h = partition (inCoset g h) G

⊢ ∀g x a b. ElGamal_decrypt g x (a,b) = |/ (a ** x) * b

⊢ ∀g y h m k. ElGamal_encrypt g y h m k = (y ** k,h ** k * m)

⊢ ∀n. Estar n = <|carrier := Euler n; id := 1; op := (λi j. i * j MOD n)|>

⊢ ∀g. FiniteAbelianGroup g ⇔ AbelianGroup g ∧ FINITE G

⊢ ∀g. FiniteGroup g ⇔ Group g ∧ FINITE G

⊢ ∀g. GFACT g = GPROD_SET g G

⊢ ∀g f s. GPI f s = ITSET (λe acc. f e * acc) s #e

⊢ ∀g a. gen a = <|carrier := {x | ∃k. x = a ** k}; op := $*; id := #e|>

⊢ ∀g s.
    gen_set s =
    <|carrier := BIGINTER (IMAGE (λh. H) {h | h ≤ g ∧ s ⊆ H}); op := $*;
      id := #e|>

⊢ ∀f g. GroupAuto f g ⇔ GroupIso f g g

⊢ ∀f g. GroupEndo f g ⇔ GroupHomo f g g

⊢ ∀f g h.
    GroupHomo f g h ⇔
    (∀x. x ∈ G ⇒ f x ∈ h.carrier) ∧
    ∀x y. x ∈ G ∧ y ∈ G ⇒ f (x * y) = h.op (f x) (f y)

⊢ ∀f g h. GroupIso f g h ⇔ GroupHomo f g h ∧ BIJ f G h.carrier

⊢ ∀g. Group g ⇔ Monoid g ∧ G* = G

⊢ ∀op id f s. OP_IMAGE op id f s = ITSET (λe acc. op (f e) acc) s id

⊢ ∀f g x.
    StabilizerGroup f g x =
    <|carrier := stabilizer f g x; op := $*; id := #e|>

⊢ ∀h g. h ≤ g ⇔ Group h ∧ Group g ∧ H ⊆ G ∧ $o = $*

⊢ ∀n. Z n = <|carrier := count n; id := 0; op := (λi j. (i + j) MOD n)|>

⊢ ∀p. Z* p = <|carrier := residue p; id := 1; op := (λi j. i * j MOD p)|>

⊢ ∀f g x y. (x ~~ y) f g ⇒ act_by f g x y ∈ G ∧ f (act_by f g x y) x = y

⊢ ∀f g X.
    (g act X) f ⇔
    ∀x. x ∈ X ⇒
        (∀a. a ∈ G ⇒ f a x ∈ X) ∧ f #e x = x ∧
        ∀a b. a ∈ G ∧ b ∈ G ⇒ f a (f b x) = f (a * b) x

⊢ ∀n. add_mod n =
      <|carrier := {i | i < n}; id := 0; op := (λi j. (i + j) MOD n)|>

⊢ ∀g. all_subgroups g = {h | h ≤ g}

⊢ ∀g h e.
    h ≤ g ∧ e ∈ CosetPartition g h ⇒ cogen g h e ∈ G ∧ e = cogen g h e * H

⊢ ∀g a s. conjugate g a s = {a * z * |/ a | z ∈ s}

⊢ ∀h g a.
    conjugate_subgroup h g a =
    <|carrier := conjugate g a H; id := #e; op := $* |>

⊢ ∀g a X. a * X = IMAGE (λz. a * z) X

⊢ ∀g h x y. x ∘ y = cogen g h x * cogen g h y * H

⊢ ∀g. cyclic g ⇔ Group g ∧ ∃z. z ∈ G ∧ ∀x. x ∈ G ⇒ ∃n. x = z ** n

⊢ ∀g. cyclic g ⇒ cyclic_gen g ∈ G ∧ ∀x. x ∈ G ⇒ ∃n. x = cyclic_gen g ** n

⊢ ∀g. cyclic_generators g = {z | z ∈ G ∧ ord z = CARD G}

⊢ ∀g x.
    cyclic g ∧ x ∈ G ⇒
    x = cyclic_gen g ** cyclic_index g x ∧
    (FINITE G ⇒ cyclic_index g x < CARD G)

⊢ ∀g x y. eq_order g x y ⇔ ord x = ord y

⊢ ∀g z. g excluding z = <|carrier := G DIFF {z}; op := $*; id := #e|>

⊢ ∀f g X. fixed_points f g X = {x | x ∈ X ∧ ∀a. a ∈ G ⇒ f a x = x}

⊢ ∀e f.
    fn_cyclic_group e f =
    <|carrier := {x | ∃n. FUNPOW f n e = x}; id := e;
      op :=
        (λx y.
             @z. ∀xi yi.
               FUNPOW f xi e = x ∧ FUNPOW f yi e = y ⇒
               FUNPOW f (xi + yi) e = z)|>

⊢ ∀g x y. x / y = x * |/ y

⊢ ∀g h x y. x == y ⇔ x / y ∈ H

⊢ ∀g f. gfun f ⇔ ∀x. x ∈ G ⇒ f x ∈ G

⊢ ∀f g h.
    homo_image f g h = <|carrier := IMAGE f G; op := h.op; id := h.id|>

⊢ ∀g h a b. inCoset g h a b ⇔ b ∈ a * H

⊢ ∀g z. g including z = <|carrier := G ∪ {z}; op := $*; id := #e|>

⊢ ∀f g h. kernel f g h = preimage f G h.id

⊢ ∀f g h.
    kernel_group f g h = <|carrier := kernel f g h; id := #e; op := $* |>

⊢ ∀g X a. left_coset g X a = a * X

⊢ ∀g s. make_group g s = <|carrier := s; op := $*; id := #e|>

⊢ ∀p. mult_mod p =
      <|carrier := {i | i ≠ 0 ∧ i < p}; id := 1;
        op := (λi j. i * j MOD p)|>

⊢ ∀f g X. multi_orbits f g X = {e | e ∈ orbits f g X ∧ ¬SING e}

⊢ ∀h g. h << g ⇔ h ≤ g ∧ ∀a z. a ∈ G ∧ z ∈ H ⇒ a * z / a ∈ H

⊢ ∀f g x. orbit f g x = IMAGE (λa. f a x) G

⊢ ∀f g X. orbits f g X = IMAGE (orbit f g) X

⊢ ∀f g1 g2 h.
    preimage_group f g1 g2 h =
    <|carrier := PREIMAGE f h ∩ g1.carrier; op := g1.op; id := g1.id|>

⊢ ∀g h. g / h = <|carrier := CosetPartition g h; op := $o; id := H|>

⊢ ∀f g x y. (x ~~ y) f g ⇔ ∃a. a ∈ G ∧ f a x = y

⊢ ∀g X a. X * a = IMAGE (λz. z * a) X

⊢ ∀g n.
    uroots n = <|carrier := {x | x ∈ G ∧ x ** n = #e}; op := $*; id := #e|>

⊢ ∀f g X. sing_orbits f g X = {e | e ∈ orbits f g X ∧ SING e}

⊢ ∀f g x. stabilizer f g x = {a | a ∈ G ∧ f a x = x}

⊢ ∀g B. sgbcross B = ITSET $o B (gen #e)

⊢ ∀g. sgbINTER g =
      <|carrier := BIGINTER (IMAGE (λh. H) {h | h ≤ g}); op := $*;
        id := #e|>

⊢ ∀g h1 h2. h1 ∘ h2 = make_group g (h1.carrier ∘ h2.carrier)

⊢ ∀h g. subgroup h g ⇔ GroupHomo I h g

⊢ ∀g B. ssbcross B = ITSET $o B {#e}

⊢ ∀g s1 s2. s1 ∘ s2 = {x * y | x ∈ s1 ∧ y ∈ s2}

⊢ ∀g s1 s2 z.
    z ∈ s1 ∘ s2 ⇒ left z ∈ s1 ∧ right z ∈ s2 ∧ z = left z * right z

⊢ ∀g s. subset_group g s = <|carrier := s; op := $*; id := #e|>

⊢ ∀s1 s2. symdiff s1 s2 = s1 ∪ s2 DIFF s1 ∩ s2

⊢ symdiff_set = <|carrier := 𝕌(:α -> bool); id := ∅; op := symdiff|>

⊢ ∀e. trivial_group e = <|carrier := {e}; id := e; op := (λx y. e)|>

⊢ ∀g. Group g ⇒
      ∀(y::G) (h::G) (m::G) k x.
        h = y ** x ⇒ ElGamal_decrypt g x (ElGamal_encrypt g y h m k) = m

⊢ ∀n. Estar n =
      <|carrier := {i | 0 < i ∧ i < n ∧ coprime n i}; id := 1;
        op := (λi j. i * j MOD n)|>

⊢ ∀n. CARD (Estar n).carrier = totient n

⊢ ∀n. 1 < n ⇒ CARD (Estar n).carrier = phi n

⊢ ∀n. (Estar n).carrier = Euler n

⊢ ∀n. (Estar n).carrier = {i | 0 < i ∧ i < n ∧ coprime n i}

⊢ ∀n x. x ∈ (Estar n).carrier ⇔ 0 < x ∧ x < n ∧ coprime n x

⊢ ∀n. (Estar n).carrier = Euler n ∧
      (∀x y. (Estar n).op x y = x * y MOD n) ∧ (Estar n).id = 1

⊢ ∀n a.
    1 < n ∧ a ∈ (Estar n).carrier ⇒ ∀k. (Estar n).exp a k = a ** k MOD n

⊢ ∀n. FINITE (Estar n).carrier

⊢ ∀n. 1 < n ⇒ FiniteAbelianGroup (Estar n)

⊢ ∀n. 1 < n ⇒ FiniteGroup (Estar n)

⊢ ∀n. 1 < n ⇒ Group (Estar n)

⊢ ∀n. (Estar n).id = 1

⊢ ∀n a.
    1 < n ∧ a < n ∧ coprime n a ⇒
    (Estar n).inv a = a ** (totient n − 1) MOD n

⊢ ∀n a.
    (Estar n).inv a =
    if 1 < n ∧ a < n ∧ coprime n a then a ** (totient n − 1) MOD n
    else FAIL ((Estar n).inv a) bad_element

⊢ ∀n. (Estar n).carrier = Euler n ∧ (Estar n).id = 1 ∧
      (∀x y. (Estar n).op x y = x * y MOD n) ∧ FINITE (Estar n).carrier ∧
      CARD (Estar n).carrier = totient n

⊢ ∀n a. 1 < n ∧ coprime a n ⇒ a ** totient n MOD n = 1

⊢ ∀n a. 1 < n ∧ a < n ∧ coprime n a ⇒ a ** totient n MOD n = 1

⊢ ∀n a. 1 < n ∧ coprime n a ⇒ a ** totient n MOD n = 1

⊢ ∀p a. prime p ⇒ a ** p MOD p = a MOD p

⊢ ∀p a. prime p ∧ 0 < a ∧ a < p ⇒ a ** (p − 1) MOD p = 1

⊢ ∀g. FiniteAbelianGroup g ⇔
      FiniteGroup g ∧ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x

⊢ ∀g. FiniteAbelianMonoid g ⇒ GFACT g ∈ G

⊢ ∀g a. FiniteAbelianGroup g ∧ a ∈ G ⇒ GFACT g = a ** CARD G * GFACT g

⊢ ∀g. (λs b. GITSET g s b) = ITSET (λe acc. e * acc)

⊢ ∀g. GPROD_SET g = GPI I

⊢ ∀g a. Group g ∧ a ∈ G ⇒ GPROD_SET g (a * G) = GPROD_SET g G

⊢ ∀g s.
    FiniteAbelianGroup g ∧ s ⊆ G ⇒
    ∀a::G.
      a ** CARD s * GPROD_SET g s * GPROD_SET g (a * (G DIFF s)) =
      GPROD_SET g G

⊢ ∀g s.
    FiniteAbelianGroup g ∧ s ⊆ G ⇒
    ∀a x::G.
      x ∉ s ⇒
      a * x * GPROD_SET g (a * (G DIFF (x INSERT s))) =
      GPROD_SET g (a * (G DIFF s))

⊢ ∀g s. (gen_set s).exp = $**

⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ gen_set (Gen a) = gen a

⊢ ∀g s. Group g ∧ s ⊆ G ⇒ Group (gen_set s)

⊢ ∀g s. s ⊆ (gen_set s).carrier

⊢ ∀g s.
    (gen_set s).carrier = BIGINTER (IMAGE (λh. H) {h | h ≤ g ∧ s ⊆ H}) ∧
    (gen_set s).op = $* ∧ (gen_set s).id = #e

⊢ ∀g s. Group g ∧ s ⊆ G ⇒ gen_set s ≤ g

⊢ ∀g s. Group g ∧ s ⊆ G ⇒ (gen_set s).carrier ⊆ G

⊢ ∀g x. Monoid g ∧ x ∈ G* ⇒ (Invertibles g).inv x = |/ x

⊢ ∀g h. h ≤ g ∧ FINITE G ⇒ CARD G = CARD H * CARD (CosetPartition g h)

⊢ ∀g h.
    h ≤ g ∧ FINITE G ⇒
    CARD G = CARD H * CARD (partition (left_coset g H) G)

⊢ ∀g h. h ≤ g ∧ FINITE G ⇒ CARD H divides CARD G

⊢ ∀op id f. OP_IMAGE op id f ∅ = id

⊢ ∀op id f x. OP_IMAGE op id f {x} = op (f x) id

⊢ ∀op id f.
    OP_IMAGE op id f ∅ = id ∧
    (FUN_COMM op f ⇒
     ∀s. FINITE s ⇒
         ∀e. OP_IMAGE op id f (e INSERT s) =
             op (f e) (OP_IMAGE op id f (s DELETE e)))

⊢ prime 2

⊢ prime 3

⊢ prime 5

⊢ prime 7

⊢ ∀f a b. s ⊆ b ∧ SURJ f a b ⇒ IMAGE f (PREIMAGE f s ∩ a) = s

⊢ ∀g h k f. h ≤ g ∧ GroupHomo f g k ⇒ GroupHomo f h k

⊢ ∀g h. h ≤ g ⇒ subgroup h g

⊢ ∀n. CARD (Z n).carrier = n

⊢ ∀n. (Z n).carrier = count n

⊢ ∀n. (Z n).carrier = {i | i < n}

⊢ ∀n x. x ∈ (Z n).carrier ⇔ x < n

⊢ ∀n. (Z n).carrier = count n ∧ (∀x y. (Z n).op x y = (x + y) MOD n) ∧
      (Z n).id = 0

⊢ ∀n. 0 < n ⇒ ∀x m. (Z n).exp x m = x * m MOD n

⊢ ∀n. FINITE (Z n).carrier

⊢ ∀n. 0 < n ⇒ FiniteAbelianGroup (Z n)

⊢ ∀n. 0 < n ⇒ FiniteGroup (Z n)

⊢ ∀n. 0 < n ⇒ Group (Z n)

⊢ ∀n. (Z n).id = 0

⊢ ∀n x. 0 < n ∧ x < n ⇒ (Z n).inv x = (n − x) MOD n

⊢ ∀n x.
    (Z n).inv x =
    if 0 < n ∧ x < n then (n − x) MOD n else FAIL ((Z n).inv x) bad_element

⊢ ∀n. (∀x. x ∈ (Z n).carrier ⇔ x < n) ∧ (Z n).id = 0 ∧
      (∀x y. (Z n).op x y = (x + y) MOD n) ∧ FINITE (Z n).carrier ∧
      CARD (Z n).carrier = n

⊢ ∀p. 0 < p ⇒ CARD (Z* p).carrier = p − 1

⊢ ∀p. (Z* p).carrier = residue p

⊢ ∀p. (Z* p).carrier = {i | 0 < i ∧ i < p}

⊢ ∀p x. x ∈ (Z* p).carrier ⇔ 0 < x ∧ x < p

⊢ ∀p. (Z* p).carrier = residue p ∧ (∀x y. (Z* p).op x y = x * y MOD p) ∧
      (Z* p).id = 1

⊢ ∀p a. prime p ∧ a ∈ (Z* p).carrier ⇒ ∀n. (Z* p).exp a n = a ** n MOD p

⊢ ∀p. FINITE (Z* p).carrier

⊢ ∀p. prime p ⇒ FiniteAbelianGroup (Z* p)

⊢ ∀p. prime p ⇒ FiniteGroup (Z* p)

⊢ ∀p. prime p ⇒ Group (Z* p)

⊢ ∀p. (Z* p).id = 1

⊢ ∀p. prime p ⇒
      ∀x. 0 < x ∧ x < p ⇒ (Z* p).inv x = (Z* p).exp x (order (Z* p) x − 1)

⊢ ∀p x.
    (Z* p).inv x =
    if prime p ∧ 0 < x ∧ x < p then (Z* p).exp x (order (Z* p) x − 1)
    else FAIL ((Z* p).inv x) bad_element

⊢ ∀p. prime p ⇒ ∀a. 0 < a ∧ a < p ⇒ (Z* p).inv a = a ** (p − 2) MOD p

⊢ ∀p a.
    (Z* p).inv a =
    if prime p ∧ 0 < a ∧ a < p then a ** (p − 2) MOD p else (Z* p).inv a

⊢ ∀p. (Z* p).carrier = residue p ∧ (Z* p).id = 1 ∧
      (∀x y. (Z* p).op x y = x * y MOD p) ∧ FINITE (Z* p).carrier ∧
      (0 < p ⇒ CARD (Z* p).carrier = p − 1)

⊢ ∀g. AbelianGroup g ⇒ AbelianMonoid g

⊢ ∀g. AbelianGroup g ⇒
      ∀x y.
        x ∈ G ∧ y ∈ G ⇒
        ∃z. z ∈ G ∧ ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y)

⊢ ∀g. AbelianGroup g ⇒
      ∀x y.
        x ∈ G ∧ y ∈ G ∧ coprime (ord x) (ord y) ⇒
        ∃z. z ∈ G ∧ ord z = ord x * ord y

⊢ ∀g. AbelianMonoid g ⇒
      ∀z. z ∉ G* ⇒ monoid_invertibles (g excluding z) = G*

⊢ ∀g h. AbelianGroup g ∧ h ≤ g ⇒ AbelianGroup h

⊢ ∀g. AbelianGroup g ⇒
      ∀h1 h2.
        h1 ≤ g ∧ h2 ≤ g ∧ FiniteGroup h1 ∧ FiniteGroup h2 ⇒
        FiniteGroup (h1 ∘ h2)

⊢ ∀g. AbelianGroup g ⇒ ∀h1 h2. h1 ≤ g ∧ h2 ≤ g ⇒ h1 ∘ h2 ≤ g

⊢ ∀f g X. (g act X) f ⇒ ∀a x. a ∈ G ∧ x ∈ X ⇒ f a x ∈ X

⊢ ∀f g X.
    (g act X) f ⇒ ∀a b x. a ∈ G ∧ b ∈ G ∧ x ∈ X ⇒ f a (f b x) = f (a * b) x

⊢ ∀f g X. (g act X) f ⇒ ∀x. x ∈ X ⇒ f #e x = x

⊢ ∀f g X x.
    Group g ∧ (g act X) f ∧ x ∈ X ⇒
    ∀a b. a ∈ G ∧ b ∈ G ⇒ (f a x = f b x ⇔ |/ a * b ∈ stabilizer f g x)

⊢ ∀f g X x.
    Group g ∧ (g act X) f ∧ x ∈ X ⇒
    ∀a b::G. f a x = f b x ⇔ |/ a * b ∈ stabilizer f g x

⊢ ∀f g X x y.
    Group g ∧ (g act X) f ∧ x ∈ X ∧ y ∈ orbit f g x ⇒
    act_by f g x y * stabilizer f g x = {a | a ∈ G ∧ f a x = y}

⊢ ∀f g X x y.
    Group g ∧ (g act X) f ∧ x ∈ X ∧ y ∈ orbit f g x ⇒
    ∀a. a ∈ G ∧ f a x = y ⇒ a * stabilizer f g x = {b | b ∈ G ∧ f b x = y}

⊢ ∀f g X.
    Group g ∧ (g act X) f ⇒
    ∀a x y. a ∈ G ∧ x ∈ X ∧ y ∈ X ∧ f a x = y ⇒ f ( |/ a) y = x

⊢ ∀f g X x. (g act X) f ∧ x ∈ X ⇒ SURJ (λa. f a x) G (orbit f g x)

⊢ ∀f g X.
    (g act X) f ⇒
    ∀a b x y z.
      a ∈ G ∧ b ∈ G ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X ∧ f a x = y ∧ f b y = z ⇒
      f (b * a) x = z

⊢ ∀n. 0 < n ⇒ AbelianGroup (add_mod n)

⊢ ∀n. CARD (add_mod n).carrier = n

⊢ ∀n. (add_mod n).carrier = {i | i < n}

⊢ ∀n. (add_mod n).carrier = count n

⊢ ∀n. 0 < n ⇒ cyclic (add_mod n)

⊢ ∀n x. x ∈ (add_mod n).carrier ⇔ x < n

⊢ ∀n. (add_mod n).carrier = {i | i < n} ∧
      (∀x y. (add_mod n).op x y = (x + y) MOD n) ∧ (add_mod n).id = 0

⊢ ∀n. 0 < n ⇒ ∀x m. (add_mod n).exp x m = x * m MOD n

⊢ ∀n. FINITE (add_mod n).carrier

⊢ ∀n. 0 < n ⇒ FiniteAbelianGroup (add_mod n)

⊢ ∀n. 0 < n ⇒ FiniteGroup (add_mod n)

⊢ ∀n. 0 < n ⇒ Group (add_mod n)

⊢ ∀n. (add_mod n).id = 0

⊢ ∀n x. 0 < n ∧ x < n ⇒ (add_mod n).inv x = (n − x) MOD n

⊢ ∀n x.
    (add_mod n).inv x =
    if 0 < n ∧ x < n then (n − x) MOD n
    else FAIL ((add_mod n).inv x) bad_element

⊢ ∀n. 1 < n ⇒ order (add_mod n) 1 = n

⊢ ∀n. (∀x. x ∈ (add_mod n).carrier ⇔ x < n) ∧ (add_mod n).id = 0 ∧
      (∀x y. (add_mod n).op x y = (x + y) MOD n) ∧
      FINITE (add_mod n).carrier ∧ CARD (add_mod n).carrier = n

⊢ ∀g h. h ∈ all_subgroups g ⇔ h ≤ g

⊢ ∀g. FiniteGroup g ⇒ FINITE (all_subgroups g)

⊢ ∀g. Group g ⇒ gen #e ∈ all_subgroups g

⊢ ∀g. Group g ⇒ IMAGE (λh. H) (all_subgroups g) ⊆ POW G

⊢ ∀f g1 g2 h1 h2.
    Group g1 ∧ Group g2 ∧ h1 ≤ g1 ∧ h2 ≤ g2 ∧ GroupHomo f g1 g2 ∧
    SURJ f g1.carrier g2.carrier ∧ kernel f g1 g2 ⊆ h1.carrier ⇒
    IMAGE f (PREIMAGE f h2.carrier ∩ g1.carrier) = h2.carrier ∧
    PREIMAGE f (IMAGE f h1.carrier) ∩ g1.carrier = h1.carrier

⊢ ∀g h. h ≤ g ∧ FINITE G ⇒ CARD G = ∑ CARD (CosetPartition g h)

⊢ ∀g h. h ≤ g ∧ FINITE G ⇒ CARD G = ∑ CARD (partition (left_coset g H) G)

⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ G ⇒ cogen g h (x * H) ∈ G

⊢ ∀h g e. h ≤ g ∧ e ∈ CosetPartition g h ⇒ cogen g h e ∈ G

⊢ ∀g h. h ≤ g ⇒ cogen g h H * H = H

⊢ ∀g h. h ≤ g ⇒ ∀a. a ∈ G ⇒ Group (conjugate_subgroup h g a)

⊢ ∀g h. h ≤ g ⇒ ∀a::G. conjugate_subgroup h g a ≤ g

⊢ ∀f g1 g2 h1 h2.
    Group g1 ∧ Group g2 ∧ GroupHomo f g1 g2 ∧
    SURJ f g1.carrier g2.carrier ∧ h1 ≤ g1 ∧ kernel f g1 g2 ⊆ h1.carrier ∧
    h2 ≤ g2 ⇒
    homo_image f h1 g2 ≤ g2 ∧ preimage_group f g1 g2 h2.carrier ≤ g1 ∧
    kernel f g1 g2 ⊆ PREIMAGE f h2.carrier ∩ g1.carrier ∧
    (h2 << g2 ⇔ preimage_group f g1 g2 h2.carrier << g1) ∧
    IMAGE f (PREIMAGE f h2.carrier ∩ g1.carrier) = h2.carrier ∧
    PREIMAGE f (IMAGE f h1.carrier) ∩ g1.carrier = h1.carrier ∧
    (FiniteGroup g1 ⇒
     CARD (preimage_group f g1 g2 h2.carrier).carrier =
     CARD h2.carrier * CARD (kernel f g1 g2))

⊢ ∀g a X. a * X = {a * z | z ∈ X}

⊢ ∀h g e. h ≤ g ∧ e ∈ CosetPartition g h ⇒ e = cogen g h e * H

⊢ ∀g X a. a ∈ G ⇒ ∀x. x ∈ a * X ⇔ ∃y. y ∈ X ∧ x = a * y

⊢ ∀g a. Group g ∧ a ∈ G ⇒ a * ∅ = ∅

⊢ ∀g h. h << g ⇒ GroupIso I (homo_group g (left_coset g H)) (g / h)

⊢ ∀g h. h ≤ g ⇒ #e * H = H

⊢ ∀g h. h ≤ g ∧ FINITE G ⇒ CARD (CosetPartition g h) = CARD G DIV CARD H

⊢ ∀g h. h ≤ g ⇒ ∀e. e ∈ CosetPartition g h ⇔ ∃a. a ∈ G ∧ e = a * H

⊢ ∀g h. h ≤ g ∧ FINITE G ⇒ ∀e. e ∈ CosetPartition g h ⇒ CARD e = CARD H

⊢ ∀g h. h ≤ g ⇒ CosetPartition g h = IMAGE (left_coset g H) G

⊢ ∀g a. Group g ∧ a ∈ G ⇒ ∀X. X ⊆ G ⇒ a * X ⊆ G

⊢ ∀g h. FiniteGroup g ∧ h << g ⇒ CARD G = CARD H * CARD (g / h).carrier

⊢ ∀g. cyclic g ⇒ ∀x. x ∈ G ⇒ ∃n. x = cyclic_gen g ** n

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      ∀x. x ∈ G ⇒ ∃n. n < CARD G ∧ x = cyclic_gen g ** n

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      ∀x. x ∈ G ⇒ x ∈ Gen (cyclic_gen g ** (CARD G DIV ord x))

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      partition (eq_order g) G = {orders g n | n | n divides CARD G}

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      partition (eq_order g) G = {orders g n | n | n ∈ divisors (CARD G)}

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      IMAGE CARD (partition (eq_order g) G) = IMAGE phi (divisors (CARD G))

⊢ ∀g. FiniteGroup g ⇒ (cyclic g ⇔ ∃z. z ∈ G ∧ ord z = CARD G)

⊢ ∀g. cyclic g ∧ FINITE G ⇒ ∀n. n divides CARD G ⇒ ∃x. x ∈ G ∧ ord x = n

⊢ ∀g. cyclic g ⇒ cyclic_gen g ∈ G

⊢ ∀g. cyclic g ∧ FINITE G ⇒ ord (cyclic_gen g) = CARD G

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      ∀n. 0 < n ∧ CARD G MOD n = 0 ⇒
          ord (cyclic_gen g ** (CARD G DIV n)) = n

⊢ ∀g. cyclic g ⇒ g = gen (cyclic_gen g)

⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ cyclic (gen x)

⊢ ∀g. cyclic g ∧ FINITE G ⇒ CARD (cyclic_generators g) = phi (CARD G)

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      BIJ (λj. cyclic_gen g ** j) (coprimes (CARD G)) (cyclic_generators g)

⊢ ∀g z. z ∈ cyclic_generators g ⇔ z ∈ G ∧ ord z = CARD G

⊢ ∀g. FINITE G ⇒ FINITE (cyclic_generators g)

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      ∀n. n divides CARD G ⇒
          cyclic_generators (gen (cyclic_gen g ** (CARD G DIV n))) =
          orders g n

⊢ ∀g. cyclic g ∧ FINITE G ⇒ cyclic_generators g ≠ ∅

⊢ ∀g. cyclic_generators g ⊆ G

⊢ ∀g. cyclic g ⇒ Group g

⊢ ∀g. cyclic g ⇒ AbelianGroup g

⊢ ∀g. cyclic g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x

⊢ ∀g. cyclic g ∧ FINITE G ⇒ IMAGE ord G = divisors (CARD G)

⊢ ∀g x.
    cyclic g ∧ x ∈ G ⇒ ∃n. x = cyclic_gen g ** n ∧ (FINITE G ⇒ n < CARD G)

⊢ ∀g h f.
    cyclic g ∧ cyclic h ∧ FINITE G ∧ GroupIso f g h ⇒
    f (cyclic_gen g) ∈ cyclic_generators h

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      ∀n. CARD (orders g n) = if n divides CARD G then phi n else 0

⊢ ∀g. cyclic g ∧ FINITE G ⇒ ∀n. n divides CARD G ⇒ orders g n ≠ ∅

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G))

⊢ ∀g. cyclic g ∧ FINITE G ⇒ ∀n. (∃h. h ≤ g ∧ CARD H = n) ⇔ n divides CARD G

⊢ ∀g h. cyclic g ∧ h ≤ g ⇒ cyclic h

⊢ ∀g. cyclic g ⇒ ∀n. cyclic (uroots n)

⊢ ∀g. FINITE G ∧ cyclic g ⇒
      ∀n. ∃z. z ∈ (uroots n).carrier ∧ ord z = CARD (uroots n).carrier

⊢ ∀g X a. a ∈ G ⇒ ∀x. x ∈ X ⇒ a * x ∈ a * X

⊢ ∀g. eq_order g equiv_on G

⊢ ∀g. eq_order g = feq ord

⊢ ∀p a. prime p ∧ 0 < a ∧ a < p ⇒ a ** (p − 1) MOD p = 1

⊢ ∀p a. prime p ⇒ a ** (p − 1) MOD p = if a MOD p = 0 then 0 else 1

⊢ ∀p. prime p ⇒ ∀a. a ** p MOD p = a MOD p

⊢ ∀p. prime p ⇒ ∀x y z. x ** p + y ** p = z ** p ⇒ (x + y) MOD p = z MOD p

⊢ ∀g a. FiniteAbelianGroup g ∧ a ∈ G ⇒ a ** CARD G = #e

⊢ ∀g. FiniteAbelianGroup g ⇒ FiniteAbelianMonoid g

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      BIJ (λn. cyclic_gen g ** n) (add_mod (CARD G)).carrier G

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      GroupHomo (λn. cyclic_gen g ** n) (add_mod (CARD G)) g

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      GroupIso (λn. cyclic_gen g ** n) (add_mod (CARD G)) g

⊢ ∀g1 g2.
    cyclic g1 ∧ cyclic g2 ∧ FINITE g1.carrier ∧ FINITE g2.carrier ∧
    CARD g1.carrier = CARD g2.carrier ⇒
    BIJ (λx. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1.carrier
      g2.carrier

⊢ ∀n. 0 < n ⇒ ∃g. cyclic g ∧ CARD g.carrier = n

⊢ ∀g1 g2.
    cyclic g1 ∧ cyclic g2 ∧ FINITE g1.carrier ∧ FINITE g2.carrier ∧
    CARD g1.carrier = CARD g2.carrier ⇒
    GroupHomo (λx. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2

⊢ ∀g1 g2.
    cyclic g1 ∧ cyclic g2 ∧ FINITE g1.carrier ∧ FINITE g2.carrier ∧
    CARD g1.carrier = CARD g2.carrier ⇒
    GroupIso (λx. g2.exp (cyclic_gen g2) (cyclic_index g1 x)) g1 g2

⊢ ∀g1 g2.
    cyclic g1 ∧ cyclic g2 ∧ FINITE g1.carrier ∧ FINITE g2.carrier ∧
    CARD g1.carrier = CARD g2.carrier ⇒
    ∃f. GroupIso f g1 g2

⊢ ∀g x y.
    cyclic g ∧ FINITE G ∧ x ∈ G ∧ y ∈ G ⇒
    cyclic_index g (x * y) =
    (cyclic_index g x + cyclic_index g y) MOD CARD G

⊢ ∀g. cyclic g ∧ FINITE G ⇒
      ∀n. n < CARD G ⇒ cyclic_index g (cyclic_gen g ** n) = n

⊢ ∀g x.
    cyclic g ∧ FINITE G ∧ x ∈ G ⇒
    ∀n. n < CARD G ⇒ (x = cyclic_gen g ** n ⇔ n = cyclic_index g x)

⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ a ** CARD G = #e

⊢ ∀g. FiniteGroup g ⇒ 0 < CARD G

⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ ∃h k. x ** h = x ** k ∧ h ≠ k

⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ ∃k. 0 < k ∧ x ** k = #e

⊢ ∀g. FiniteGroup g ⇒ FiniteMonoid g

⊢ ∀g. FiniteGroup g ⇒ Group g

⊢ ∀g. FiniteGroup g ⇒ Monoid g

⊢ ∀g. FiniteGroup g ⇒
      ∀x. x ∈ G ⇒
          ∀n. ord x = n ⇒
              0 < n ∧ x ** n = #e ∧ ∀m. 0 < m ∧ m < n ⇒ x ** m ≠ #e

⊢ ∀g. FiniteGroup g ⇒
      ∀z. z ∈ G ∧ ord z = CARD G ⇒ ∀x. x ∈ G ⇒ ∃n. n < CARD G ∧ x = z ** n

⊢ ∀f g1 g2 h.
    FiniteGroup g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ⇒
    FINITE (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier

⊢ ∀g. FiniteMonoid g ⇒ FiniteGroup (Invertibles g)

⊢ ∀g. FiniteGroup g ⇒ ∀h. h ≤ g ⇒ FINITE H

⊢ ∀g. FiniteGroup g ⇒ ∀h. h ≤ g ⇒ FiniteGroup h

⊢ ∀f g X x. x ∈ fixed_points f g X ⇔ x ∈ X ∧ ∀a. a ∈ G ⇒ f a x = x

⊢ ∀f g X x. x ∈ fixed_points f g X ⇒ x ∈ X

⊢ ∀f g X. FINITE X ⇒ FINITE (fixed_points f g X)

⊢ ∀f g X.
    Group g ∧ (g act X) f ⇒
    ∀x. x ∈ X ⇒ (x ∈ fixed_points f g X ⇔ SING (orbit f g x))

⊢ ∀f g X.
    Group g ∧ (g act X) f ⇒
    ∀x. x ∈ fixed_points f g X ⇔ x ∈ X ∧ orbit f g x = {x}

⊢ ∀f g X. fixed_points f g X ⊆ X

⊢ ∀e f n.
    (∃k. k ≠ 0 ∧ FUNPOW f k e = e) ∧
    n = (LEAST k. k ≠ 0 ∧ FUNPOW f k e = e) ⇒
    (fn_cyclic_group e f).carrier = {FUNPOW f k e | k < n} ∧
    (fn_cyclic_group e f).id = e ∧
    ∀i j.
      (fn_cyclic_group e f).op (FUNPOW f i e) (FUNPOW f j e) =
      FUNPOW f ((i + j) MOD n) e

⊢ ∀e f. (fn_cyclic_group e f).carrier = {x | ∃n. FUNPOW f n e = x}

⊢ ∀e f.
    (∃n. n ≠ 0 ∧ FUNPOW f n e = e) ⇒
    FiniteAbelianGroup (fn_cyclic_group e f)

⊢ ∀e f. (∃n. n ≠ 0 ∧ FUNPOW f n e = e) ⇒ FiniteGroup (fn_cyclic_group e f)

⊢ ∀e f. (∃n. n ≠ 0 ∧ FUNPOW f n e = e) ⇒ Group (fn_cyclic_group e f)

⊢ ∀e f. (fn_cyclic_group e f).id = e

⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ ∀x. x ∈ Gen a ⇒ x ** CARD (Gen a) = #e

⊢ ∀g a. a ∈ G ⇒ Gen a = IMAGE ($** a) 𝕌(:num)

⊢ ∀g. Group g ⇒
      ∀a. a ∈ G ∧ 0 < ord a ⇒ Gen a = IMAGE (λj. a ** j) (count (ord a))

⊢ ∀g a. #e ∈ Gen a

⊢ ∀g a x. x ∈ Gen a ⇔ ∃n. x = a ** n

⊢ ∀g a z. a ∈ G ∧ z ∈ Gen a ⇒ ∀n. (gen a).exp z n = z ** n

⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ FiniteGroup (gen a)

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x ∈ Gen x

⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ Group (gen a)

⊢ ∀g a. Group g ∧ a ∈ G ∧ 0 < ord a ⇒ CARD (Gen a) = ord a

⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ FINITE (Gen a)

⊢ ∀g. Group g ⇒ Gen #e = {#e}

⊢ ∀g. Group g ⇒ gen #e ≤ g

⊢ ∀g. FiniteGroup g ⇒ ∀s. s ⊆ G ⇒ IMAGE gen s ⊆ all_subgroups g

⊢ ∀g. Group g ⇒ ∀s. s ⊆ G ⇒ IMAGE (λa. Gen a) s ⊆ POW G

⊢ ∀g a. (gen a).op = $* ∧ (gen a).id = #e

⊢ ∀g a. FiniteGroup g ∧ a ∈ G ⇒ gen a ≤ g

⊢ ∀g a. Group g ∧ a ∈ G ⇒ Gen a ⊆ G

⊢ ∀g. Group g ⇒ G* = G

⊢ ∀g. Group g ⇔
      (∀x y::G. x * y ∈ G) ∧ (∀x y z::G. x * y * z = x * (y * z)) ∧
      #e ∈ G ∧ (∀x::G. #e * x = x) ∧ ∀x::G. |/ x ∈ G ∧ |/ x * x = #e

⊢ ∀g. Group g ⇒ ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x * y * z = x * (y * z)

⊢ ∀g. GroupAuto I g

⊢ ∀g f. GroupAuto f g ⇒ f PERMUTES G

⊢ ∀g f1 f2. GroupAuto f1 g ∧ GroupAuto f2 g ⇒ GroupAuto (f1 ∘ f2) g

⊢ ∀f g. GroupAuto f g ⇒ ∀x. x ∈ G ⇒ f x ∈ G

⊢ ∀g f. Group g ∧ GroupAuto f g ⇒ ∀x. x ∈ G ⇒ ∀n. f (x ** n) = f x ** n

⊢ ∀f g. Group g ∧ GroupAuto f g ⇒ f #e = #e

⊢ ∀g f. Group g ∧ GroupAuto f g ⇒ MonoidAuto f g

⊢ ∀g f. Group g ∧ GroupAuto f g ⇒ GroupAuto (LINV f G) g

⊢ ∀g f. Group g ∧ GroupAuto f g ⇒ ∀x. x ∈ G ⇒ ord (f x) = ord x

⊢ ∀g. Group g ⇒ G ≠ ∅

⊢ ∀g. Group g ⇒
      ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x ⇒ ∀n. x ** n * y = y * x ** n

⊢ ∀g. Group g ⇒
      ∀x y.
        x ∈ G ∧ y ∈ G ∧ x * y = y * x ⇒
        ∀n m. x ** n * y ** m = y ** m * x ** n

⊢ ∀g. Group g ⇒
      ∀x y.
        x ∈ G ∧ y ∈ G ∧ x * y = y * x ⇒ ∀n. (x * y) ** n = x ** n * y ** n

⊢ ∀g a. Group g ∧ a ∈ G ⇒ a * G = G

⊢ ∀g a. Group g ∧ a ∈ G ⇒ a * G = G

⊢ ∀g. Group g ⇔
      (∀x y. x ∈ G ∧ y ∈ G ⇒ x * y ∈ G) ∧
      (∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x * y * z = x * (y * z)) ∧ #e ∈ G ∧
      (∀x. x ∈ G ⇒ #e * x = x) ∧ ∀x. x ∈ G ⇒ ∃y. y ∈ G ∧ y * x = #e

⊢ ∀g. Group g ⇔ Monoid g ∧ ∀x. x ∈ G ⇒ ∃y. y ∈ G ∧ y * x = #e

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x / x = #e

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ x / y ∈ G

⊢ ∀g. Group g ⇒
      ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ z * x / (z * y) = z * (x / y) / z

⊢ ∀g. Group g ⇒
      ∀x1 y1 x2 y2.
        x1 ∈ G ∧ y1 ∈ G ∧ x2 ∈ G ∧ y2 ∈ G ⇒
        x1 * y1 / (x2 * y2) = x1 * (y1 / y2) / x1 * (x1 / x2)

⊢ ∀g. Group g ⇒ ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x * z / (y * z) = x / y

⊢ ∀g z x n. (g excluding z).exp x n = x ** n

⊢ ∀g z. (g excluding z).op = $*

⊢ ∀g z.
    (g excluding z).op = $* ∧ (g excluding z).id = #e ∧
    ∀x. x ∈ (g excluding z).carrier ⇒ x ∈ G ∧ x ≠ z

⊢ ∀g x. x ** 0 = #e

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x ** 1 = x

⊢ ∀g x n. x ** SUC n = x * x ** n

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n k. x ** (n + k) = x ** n * x ** k

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. x ** n * x = x * x ** n

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. x ** n ∈ G

⊢ ∀g. Group g ⇒
      ∀x. x ∈ G ⇒ ∀m n. m < n ∧ x ** m = x ** n ⇒ x ** (n − m) = #e

⊢ ∀g x.
    Group g ∧ x ∈ G ∧ 0 < ord x ⇒
    ∀n m. x ** n = x ** m ⇔ n MOD ord x = m MOD ord x

⊢ ∀g x.
    Group g ∧ x ∈ G ⇒ ∀n m. n < ord x ∧ m < ord x ∧ x ** n = x ** m ⇒ n = m

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. |/ (x ** n) = |/ x ** n

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ∧ 0 < ord x ⇒ ∀n. x ** n = x ** (n MOD ord x)

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ∧ 0 < ord x ⇒ ∀n. x ** n = x ** (n MOD ord x)

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n k. x ** (n * k) = (x ** n) ** k

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀m n. (x ** m) ** n = (x ** n) ** m

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. x ** SUC n = x ** n * x

⊢ ∀g h f.
    Group g ∧ Group h ∧ GroupHomo f g h ⇒
    kernel_group f g h << g ∧ homo_image f g h ≤ h ∧
    GroupIso (λz. CHOICE (preimage f G z) * kernel f g h)
      (homo_image f g h) (g / kernel_group f g h) ∧
    (SURJ f G h.carrier ⇒ GroupIso I h (homo_image f g h))

⊢ ∀g. GroupHomo I g g

⊢ ∀g h k f1 f2.
    GroupHomo f1 g h ∧ GroupHomo f2 h k ⇒ GroupHomo (f2 ∘ f1) g k

⊢ ∀g h f1 f2.
    Group g ∧ Group h ∧ (∀x. x ∈ G ⇒ f1 x = f2 x) ⇒
    (GroupHomo f1 g h ⇔ GroupHomo f2 g h)

⊢ ∀f g h. GroupHomo f g h ⇒ ∀x. x ∈ G ⇒ f x ∈ h.carrier

⊢ ∀g h f.
    Group g ∧ Group h ∧ GroupHomo f g h ⇒
    ∀x. x ∈ G ⇒ ∀n. f (x ** n) = h.exp (f x) n

⊢ ∀g h f. Group g ∧ MonoidHomo f g h ⇒ Group (homo_image f g h)

⊢ ∀f g h. Group g ∧ Group h ∧ GroupHomo f g h ⇒ f #e = h.id

⊢ ∀g h f.
    Group g ∧ Group h ∧ SURJ f G h.carrier ⇒
    GroupIso I h (homo_image f g h)

⊢ ∀f g h.
    Group g ∧ Group h ∧ GroupHomo f g h ⇒
    ∀x. x ∈ G ⇒ f ( |/ x) = h.inv (f x)

⊢ ∀g h f. Group g ∧ Group h ∧ GroupHomo f g h ⇒ MonoidHomo f g h

⊢ ∀f g h. GroupHomo f g h ∧ f #e = h.id ⇔ MonoidHomo f g h

⊢ ∀g h f.
    Group g ∧ GroupHomo f g h ∧ BIJ f G h.carrier ⇒
    GroupHomo (LINV f G) h g

⊢ Group g ∧ GroupHomo f g h ∧ (∀x. x ∈ h.carrier ⇒ i x ∈ G ∧ f (i x) = x) ∧
  (∀x. x ∈ G ⇒ i (f x) = x) ⇒
  GroupHomo i h g

⊢ ∀g h k f1 f2.
    GroupHomo f1 g h ∧ GroupHomo f2 h k ⇒ GroupHomo (f2 ∘ f1) g k

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ #e * x = x ∧ x * #e = x

⊢ ∀g. Group g ⇒ #e ∈ G

⊢ ∀g. Group g ⇒ ∀n. #e ** n = #e

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ (x * x = x ⇔ x = #e)

⊢ ∀g. Group g ⇒ #e * #e = #e

⊢ ∀g. Group g ⇒
      ∀x y. x ∈ G ∧ y ∈ G ⇒ (y * x = x ⇔ y = #e) ∧ (x * y = x ⇔ y = #e)

⊢ ∀g. GPI = OP_IMAGE $* #e

⊢ ∀g f. GPI f ∅ = #e

⊢ ∀g. Monoid g ⇒ ∀f. gfun f ⇒ ∀x. x ∈ G ⇒ GPI f {x} = f x

⊢ ∀g z. z ∉ G ⇒ (AbelianGroup g ⇔ AbelianGroup (g including z excluding z))

⊢ ∀g z.
    g including z excluding z =
    if z ∈ G then <|carrier := G DELETE z; op := $*; id := #e|> else g

⊢ ∀g z. z ∉ G ⇒ (Group g ⇔ Group (g including z excluding z))

⊢ ∀g z.
    (g including z excluding z).op = $* ∧
    (g including z excluding z).id = #e ∧
    (z ∉ G ⇒ (g including z excluding z).carrier = G)

⊢ ∀g z.
    (g including z).op = $* ∧ (g including z).id = #e ∧
    ∀x. x ∈ (g including z).carrier ⇒ x ∈ G ∨ x = z

⊢ ∀g f.
    AbelianGroup g ∧ INJ f G 𝕌(:β) ⇒ AbelianGroup (monoid_inj_image g f)

⊢ ∀g f e.
    AbelianGroup (g excluding e) ∧ INJ f G 𝕌(:β) ∧ e ∈ G ⇒
    AbelianGroup (monoid_inj_image g f excluding f e)

⊢ ∀g f e.
    Group (g excluding e) ∧ INJ f G 𝕌(:β) ∧ e ∈ G ⇒
    Group (monoid_inj_image g f excluding f e)

⊢ ∀g f. Group g ∧ INJ f G 𝕌(:β) ⇒ Group (monoid_inj_image g f)

⊢ ∀g f. INJ f G 𝕌(:β) ⇒ GroupHomo f g (monoid_inj_image g f)

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ |/ x ∈ G

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ ( |/ x = |/ y ⇔ x = y)

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ( |/ x = #e ⇔ x = #e)

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ ( |/ x = y ⇔ x = |/ y)

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. |/ x ** n = |/ (x ** n)

⊢ ∀g. Group g ⇒ |/ #e = #e

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ |/ ( |/ x) = x

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ |/ (x * y) = |/ y * |/ x

⊢ ∀g x. Group g ∧ x ∈ G ⇒ ord ( |/ x) = ord x

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x * |/ x = #e ∧ |/ x * x = #e

⊢ ∀g. Group g ⇒ Monoid g

⊢ ∀g. GroupIso I g g

⊢ ∀g h f. GroupIso f g h ⇒ BIJ f G h.carrier

⊢ ∀g h f. GroupIso f g h ∧ FINITE G ⇒ CARD G = CARD h.carrier

⊢ ∀g h k f1 f2. GroupIso f1 g h ∧ GroupIso f2 h k ⇒ GroupIso (f2 ∘ f1) g k

⊢ ∀f g h. GroupIso f g h ⇒ ∀x. x ∈ G ⇒ f x ∈ h.carrier

⊢ ∀g h f.
    Group g ∧ Group h ∧ GroupIso f g h ⇒
    ∀x. x ∈ G ⇒ ∀n. f (x ** n) = h.exp (f x) n

⊢ ∀g h f. Group g ∧ GroupIso f g h ∧ f #e = h.id ⇒ Group h

⊢ ∀f g h. Group g ∧ Group h ∧ GroupIso f g h ⇒ f #e = h.id

⊢ ∀g h f. Group g ∧ Group h ∧ GroupIso f g h ⇒ MonoidIso f g h

⊢ ∀g h f. Group g ∧ GroupIso f g h ⇒ GroupIso (LINV f G) h g

⊢ ∀f g h. GroupIso f g h ∧ f #e = h.id ⇔ MonoidIso f g h

⊢ ∀g h f.
    Group g ∧ Group h ∧ GroupIso f g h ⇒ ∀x. x ∈ G ⇒ order h (f x) = ord x

⊢ ∀f g h.
    GroupIso f g h ⇔
    GroupHomo f g h ∧ ∀y. y ∈ h.carrier ⇒ ∃!x. x ∈ G ∧ f x = y

⊢ ∀g h f. Group g ∧ GroupIso f g h ⇒ GroupIso (LINV f G) h g

⊢ ∀g h k f1 f2. GroupIso f1 g h ∧ GroupIso f2 h k ⇒ GroupIso (f2 ∘ f1) g k

⊢ ∀g. Group g ⇒ ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ (x * y = x * z ⇔ y = z)

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ #e * x = x

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (y * x = x ⇔ y = #e)

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ |/ x * x = #e

⊢ ∀g. Group g ⇒
      ∀x y. x ∈ G ∧ y ∈ G ⇒ y = x * ( |/ x * y) ∧ y = |/ x * (x * y)

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * y = #e ⇔ x = |/ y)

⊢ ∀g. Group g ⇒ ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ (x * y = z ⇔ x = z * |/ y)

⊢ ∀g h. h << g ⇒ $== equiv_on G

⊢ ∀h g. h << g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x == y ⇔ x ∈ y * H)

⊢ ∀g h. h << g ⇒ ∀z. z ∈ G ⇒ z == z

⊢ ∀g h. h << g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x == y ⇔ y == x)

⊢ ∀g h. h << g ⇒ ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x == y ∧ y == z ⇒ x == z

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y ∈ G

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ ( |/ x * y = #e ⇔ x = y)

⊢ ∀g. Group g ⇒ ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ ( |/ x * y = z ⇔ y = x * z)

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * |/ y = #e ⇔ x = y)

⊢ ∀g. Group g ⇒ ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ (x * |/ y = z ⇔ x = z * y)

⊢ ∀g. Group g ⇒
      ∀x n.
        x ∈ G ∧ 0 < ord x ∧ n divides ord x ⇒ ord (x ** (ord x DIV n)) = n

⊢ ∀g. Group g ⇒
      ∀x y.
        x ∈ G ∧ y ∈ G ∧ x * y = y * x ⇒
        ∃z. z ∈ G ∧ ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y)

⊢ ∀g. Group g ⇒
      ∀x y.
        x ∈ G ∧ y ∈ G ∧ x * y = y * x ∧ coprime (ord x) (ord y) ⇒
        ∃z. z ∈ G ∧ ord z = ord x * ord y

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀m. x ** m = #e ⇔ ord x divides m

⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ ord x divides CARD G

⊢ ∀g x. Group g ∧ x ∈ G ⇒ ∀n. x ** n = #e ⇔ ord x divides n

⊢ ∀g. FiniteAbelianGroup g ⇒ ∀x. x ∈ G ⇒ ord x divides maximal_order g

⊢ ∀g. Group g ⇒
      ∀x m. x ∈ G ∧ 0 < ord x ∧ m divides ord x ⇒ ∃y. y ∈ G ∧ ord y = m

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ (ord x = 1 ⇔ x = #e)

⊢ ∀g x n.
    Group g ∧ x ∈ G ∧ 0 < ord x ∧ n divides ord x ⇒
    ord (x ** (ord x DIV n)) = n

⊢ ∀g. Group g ⇒ ord #e = 1

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ∧ 0 < ord x ⇒ |/ x = x ** (ord x − 1)

⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ ord x ≠ 0

⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ 0 < ord x

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀k. ord (x ** k) * gcd (ord x) k = ord x

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀n. coprime n (ord x) ⇒ ord (x ** n) = ord x

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ ∀k. ord (x ** k) = 0 ⇔ 0 < k ∧ ord x = 0

⊢ ∀g x.
    Group g ∧ x ∈ G ∧ 0 < ord x ⇒
    ∀k. ord (x ** k) = ord x ⇔ coprime k (ord x)

⊢ ∀g. Group g ⇒
      ∀x k. x ∈ G ∧ 0 < k ⇒ ord (x ** k) = ord x DIV gcd k (ord x)

⊢ ∀g. FiniteGroup g ⇒ ∀x. x ∈ G ⇒ 0 < ord x ∧ x ** ord x = #e

⊢ ∀g n.
    0 < n ⇒ ∀x. ord x = n ⇔ x ** n = #e ∧ ∀m. 0 < m ∧ m < n ⇒ x ** m ≠ #e

⊢ ∀g a.
    Group g ∧ a ∈ G ∧ 0 < ord a ⇒ BIJ (λn. a ** n) (count (ord a)) (Gen a)

⊢ ∀g. Group g ⇒
      ∀x. x ∈ G ⇒ ∀m n. m < ord x ∧ n < ord x ∧ x ** m = x ** n ⇒ m = n

⊢ ∀g. Group g ⇒ orders g 1 = {#e}

⊢ ∀g. Group g ⇒
      ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ x * z * |/ (y * z) = x * |/ y

⊢ ∀g. Group g ⇒ ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ (y * x = z * x ⇔ y = z)

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x * #e = x

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * y = x ⇔ y = #e)

⊢ ∀g. Group g ⇒ ∀x. x ∈ G ⇒ x * |/ x = #e

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ y = y * |/ x * x ∧ y = y * x * |/ x

⊢ ∀g. Group g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * y = #e ⇔ y = |/ x)

⊢ ∀g. Group g ⇒ ∀x y z. x ∈ G ∧ y ∈ G ∧ z ∈ G ⇒ (x * y = z ⇔ y = |/ x * z)

⊢ ∀g. AbelianGroup g ⇒ ∀n. Group (uroots n)

⊢ ∀g. Group g ⇒ ∀n. #e ∈ (uroots n).carrier

⊢ ∀g. AbelianGroup g ⇒ ∀n. uroots n ≤ g

⊢ ∀f g1 g2 h.
    FiniteGroup g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ⇒
    CARD (preimage_group f g1 g2 h.carrier).carrier =
    CARD (kernel_group f (preimage_group f g1 g2 h.carrier) g2).carrier *
    CARD
      (preimage_group f g1 g2 h.carrier /
       kernel_group f (preimage_group f g1 g2 h.carrier) g2).carrier

⊢ ∀g f.
    AbelianGroup g ∧ GroupHomo f g (homo_group g f) ⇒
    AbelianGroup (homo_group g f)

⊢ ∀g f.
    Group g ∧ GroupHomo f g (homo_group g f) ⇒
    ∀x y z. x ∈ fG ∧ y ∈ fG ∧ z ∈ fG ⇒ (x ∘ y) ∘ z = x ∘ y ∘ z

⊢ ∀g f. Group g ∧ INJ f G 𝕌(:β) ⇒ GroupHomo f g (homo_group g f)

⊢ ∀g f.
    Group g ∧ GroupHomo f g (homo_group g f) ⇒
    ∀x y. x ∈ fG ∧ y ∈ fG ⇒ x ∘ y ∈ fG

⊢ ∀g f.
    AbelianGroup g ∧ GroupHomo f g (homo_group g f) ⇒
    ∀x y. x ∈ fG ∧ y ∈ fG ⇒ x ∘ y = y ∘ x

⊢ ∀g f. Group g ∧ GroupHomo f g (homo_group g f) ⇒ Group (homo_group g f)

⊢ ∀g f.
    Group g ∧ GroupHomo f g (homo_group g f) ⇒
    #i ∈ fG ∧ ∀x. x ∈ fG ⇒ #i ∘ x = x ∧ x ∘ #i = x

⊢ ∀g f.
    Group g ∧ GroupHomo f g (homo_group g f) ⇒
    ∀x. x ∈ fG ⇒ ∃z. z ∈ fG ∧ z ∘ x = #i

⊢ ∀g h f. Group g ∧ Group h ∧ GroupHomo f g h ⇒ Group (homo_image f g h)

⊢ ∀g h f.
    Group g ∧ Group h ∧ GroupHomo f g h ⇒
    GroupHomo (λz. CHOICE (preimage f G z) * kernel f g h)
      (homo_image f g h) (g / kernel_group f g h)

⊢ ∀g h f.
    Group g ∧ Group h ∧ GroupHomo f g h ⇒
    GroupIso (λz. CHOICE (preimage f G z) * kernel f g h)
      (homo_image f g h) (g / kernel_group f g h)

⊢ ∀g h f.
    Monoid g ∧ Monoid h ∧ MonoidHomo f g h ⇒ Monoid (homo_image f g h)

⊢ ∀g h f. Group g ∧ Group h ∧ GroupHomo f g h ⇒ homo_image f g h ≤ h

⊢ ∀g h f.
    Group g ∧ Group h ∧ GroupHomo f g h ⇒
    BIJ (λz. CHOICE (preimage f G z) * kernel f g h)
      (homo_image f g h).carrier (g / kernel_group f g h).carrier

⊢ ∀f g1 g2 h.
    H ⊆ g1.carrier ∧ GroupHomo f g1 g2 ∧ kernel f g1 g2 ⊆ H ⇒
    kernel f g1 g2 = kernel f h g2

⊢ ∀f g1 g2 h.
    Group g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ⇒
    GroupIso
      (λz.
           coset (preimage_group f g1 g2 h.carrier)
             (CHOICE
                (preimage f (preimage_group f g1 g2 h.carrier).carrier z))
             (kernel f (preimage_group f g1 g2 h.carrier) g2))
      (homo_image f (preimage_group f g1 g2 h.carrier) g2)
      (preimage_group f g1 g2 h.carrier /
       kernel_group f (preimage_group f g1 g2 h.carrier) g2)

⊢ ∀f g1 g2 h.
    Group g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ∧
    SURJ f g1.carrier g2.carrier ⇒
    IMAGE f (PREIMAGE f h.carrier ∩ g1.carrier) = h.carrier

⊢ ∀f g1 g2 h.
    FiniteGroup g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ⇒
    CARD (homo_image f (preimage_group f g1 g2 h.carrier) g2).carrier =
    CARD
      (preimage_group f g1 g2 h.carrier /
       kernel_group f (preimage_group f g1 g2 h.carrier) g2).carrier

⊢ ∀g1 g2 h f.
    Group g1 ∧ Group g2 ∧ GroupHomo f g1 g2 ∧ h ≤ g1 ⇒
    homo_image f h g2 ≤ g2

⊢ ∀g h. h ≤ g ⇒ inCoset g h equiv_on G

⊢ ∀g h. h ≤ g ⇒ ∀a. a ∈ G ⇒ inCoset g h a a

⊢ ∀g h. h ≤ g ⇒ ∀a b. a ∈ G ∧ b ∈ G ∧ inCoset g h a b ⇒ inCoset g h b a

⊢ ∀g h.
    h ≤ g ⇒
    ∀a b c.
      a ∈ G ∧ b ∈ G ∧ c ∈ G ∧ inCoset g h a b ∧ inCoset g h b c ⇒
      inCoset g h a c

⊢ ∀g X a. a ∈ G ⇒ ∀x. x ∈ a * X ⇔ ∃y. y ∈ X ∧ x = a * y

⊢ ∀g. Group g ⇒
      ∀a b. a ∈ G ∧ b ∈ G ∧ independent g a b ⇒ (gen a = gen b ⇔ a = b)

⊢ ∀g. FiniteGroup g ⇒
      ∀a b.
        a ∈ G ∧ b ∈ G ∧ independent g a b ⇒
        CARD (gen a ∘ gen b).carrier = ord a * ord b

⊢ ∀g a b. independent g a b ⇔ independent g b a

⊢ ∀f g h. FINITE G ∧ GroupIso f g h ⇒ CARD G = CARD h.carrier

⊢ ∀g h f x. x ∈ kernel f g h ⇔ x ∈ G ∧ f x = h.id

⊢ ∀g h f. Group g ∧ Group h ∧ GroupHomo f g h ⇒ Group (kernel_group f g h)

⊢ ∀g h f. Group g ∧ Group h ∧ GroupHomo f g h ⇒ kernel_group f g h << g

⊢ ∀g h f. Group g ∧ Group h ∧ GroupHomo f g h ⇒ kernel_group f g h ≤ g

⊢ ∀g h f x. x ∈ kernel f g h ⇔ x ∈ G ∧ f x = h.id

⊢ ∀g h f.
    Group g ∧ Group h ∧ GroupHomo f g h ⇒ Group (g / kernel_group f g h)

⊢ ∀g X a. left_coset g X a = {a * z | z ∈ X}

⊢ ∀g s.
    (make_group g s).carrier = s ∧ (make_group g s).op = $* ∧
    (make_group g s).id = #e

⊢ ∀g h f. Monoid g ∧ MonoidHomo f g h ⇒ Monoid (homo_image f g h)

⊢ ∀g. Monoid g ⇒ |/ #e = #e

⊢ ∀g x. Monoid g ∧ x ∈ G* ⇒ ord ( |/ x) = ord x

⊢ ∀g. FiniteMonoid g ⇒ ∀x. x ∈ G* ⇒ 0 < ord x ∧ x ** ord x = #e

⊢ ∀g. Monoid g ⇒ Group (Invertibles g)

⊢ ∀p. prime p ⇒ AbelianGroup (mult_mod p)

⊢ ∀p. 0 < p ⇒ CARD (mult_mod p).carrier = p − 1

⊢ ∀p. (mult_mod p).carrier = {i | i ≠ 0 ∧ i < p}

⊢ ∀p. (mult_mod p).carrier = residue p

⊢ ∀p x. x ∈ (mult_mod p).carrier ⇔ x ≠ 0 ∧ x < p

⊢ ∀p x. x ∈ (mult_mod p).carrier ⇔ 0 < x ∧ x < p

⊢ ∀p. (mult_mod p).carrier = {i | i ≠ 0 ∧ i < p} ∧
      (∀x y. (mult_mod p).op x y = x * y MOD p) ∧ (mult_mod p).id = 1

⊢ ∀p a.
    prime p ∧ a ∈ (mult_mod p).carrier ⇒
    ∀n. (mult_mod p).exp a n = a ** n MOD p

⊢ ∀p. FINITE (mult_mod p).carrier

⊢ ∀p. prime p ⇒ FiniteAbelianGroup (mult_mod p)

⊢ ∀p. prime p ⇒ FiniteGroup (mult_mod p)

⊢ ∀p. prime p ⇒ Group (mult_mod p)

⊢ ∀p. (mult_mod p).id = 1

⊢ ∀p. prime p ⇒
      ∀x. 0 < x ∧ x < p ⇒
          (mult_mod p).inv x =
          (mult_mod p).exp x (order (mult_mod p) x − 1)

⊢ ∀p x.
    (mult_mod p).inv x =
    if prime p ∧ 0 < x ∧ x < p then
      (mult_mod p).exp x (order (mult_mod p) x − 1)
    else FAIL ((mult_mod p).inv x) bad_element

⊢ ∀p. prime p ⇒ ∀a. 0 < a ∧ a < p ⇒ (mult_mod p).inv a = a ** (p − 2) MOD p

⊢ ∀p a.
    (mult_mod p).inv a =
    if prime p ∧ 0 < a ∧ a < p then a ** (p − 2) MOD p
    else (mult_mod p).inv a

⊢ ∀p. (∀x. x ∈ (mult_mod p).carrier ⇒ x ≠ 0) ∧
      (∀x. x ∈ (mult_mod p).carrier ⇔ 0 < x ∧ x < p) ∧
      (mult_mod p).id = 1 ∧ (∀x y. (mult_mod p).op x y = x * y MOD p) ∧
      FINITE (mult_mod p).carrier ∧
      (0 < p ⇒ CARD (mult_mod p).carrier = p − 1)

⊢ ∀f g X e. e ∈ multi_orbits f g X ⇔ e ∈ orbits f g X ∧ ¬SING e

⊢ ∀f g X e. (g act X) f ∧ FINITE X ∧ e ∈ multi_orbits f g X ⇒ FINITE e

⊢ ∀f g X e. (g act X) f ∧ e ∈ multi_orbits f g X ⇒ e ⊆ X

⊢ ∀f g X. FINITE X ⇒ FINITE (multi_orbits f g X)

⊢ ∀f g X. multi_orbits f g X ⊆ orbits f g X

⊢ ∀f g X.
    FINITE X ⇒
    CARD (X DIFF fixed_points f g X) = CARD X − CARD (fixed_points f g X)

⊢ ∀f g X.
    Group g ∧ (g act X) f ⇒
    ∀x. x ∈ X DIFF fixed_points f g X ⇔ x ∈ X ∧ ¬SING (orbit f g x)

⊢ ∀g h. h << g ⇒ ∀x. x ∈ G ⇒ x / cogen g h (x * H) ∈ H

⊢ ∀g h.
    h << g ⇒
    ∀x y.
      x ∈ CosetPartition g h ∧ y ∈ CosetPartition g h ⇒
      x ∘ y =
      CHOICE (preimage (left_coset g H) G x) *
      CHOICE (preimage (left_coset g H) G y) * H

⊢ ∀g h.
    h << g ⇒
    ∀a b.
      a ∈ G ∧ b ∈ G ⇒ cogen g h (a * H) * cogen g h (b * H) * H = a * b * H

⊢ ∀g h.
    h << g ⇒ ∀a b. a ∈ G ∧ b ∈ G ⇒ cogen g h (a * H) * b * H = a * b * H

⊢ ∀g h.
    h << g ⇒ ∀a b. a ∈ G ∧ b ∈ G ⇒ a * cogen g h (b * H) * H = a * b * H

⊢ ∀f g1 g2 h2.
    Group g1 ∧ Group g2 ∧ h2 ≤ g2 ∧ GroupHomo f g1 g2 ∧
    SURJ f g1.carrier g2.carrier ⇒
    (h2 << g2 ⇔ preimage_group f g1 g2 h2.carrier << g1)

⊢ ∀f g1 g2 h2.
    Group g1 ∧ Group g2 ∧ h2 ≤ g2 ∧ GroupHomo f g1 g2 ⇒
    h2 << g2 ⇒
    preimage_group f g1 g2 h2.carrier << g1

⊢ ∀g h. h << g ⇔ h ≤ g ∧ ∀a. a ∈ G ⇒ a * H = H * a

⊢ ∀g h. h << g ∧ g << h ⇒ h = g

⊢ ∀g h. h << g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * H = y * H ⇔ x / y ∈ H)

⊢ ∀g h. h << g ⇒ GroupHomo (left_coset g H) g (g / h)

⊢ ∀g h. h << g ⇒ h ≤ g ∧ Group h ∧ Group g

⊢ ∀h g. h << g ⇒ ∀a z. a ∈ G ∧ z ∈ H ⇒ a * z / a ∈ H

⊢ ∀g. Group g ⇒ g << g

⊢ ∀h g. h << g ⇒ h ≤ g

⊢ ∀f g1 g2 h2.
    Group g1 ∧ Group g2 ∧ h2 ≤ g2 ∧ GroupHomo f g1 g2 ∧
    SURJ f g1.carrier g2.carrier ⇒
    preimage_group f g1 g2 h2.carrier << g1 ⇒
    h2 << g2

⊢ ∀f g x. orbit f g x = {f a x | a ∈ G}

⊢ ∀f g X x.
    FiniteGroup g ∧ (g act X) f ∧ x ∈ X ∧ FINITE X ⇒
    CARD (orbit f g x) divides CARD G

⊢ ∀f g x y. y ∈ orbit f g x ⇔ (x ~~ y) f g

⊢ ∀f g X x y. (g act X) f ∧ x ∈ X ∧ y ∈ orbit f g x ⇒ y ∈ X

⊢ ∀f g X x. (g act X) f ∧ x ∈ X ⇒ orbit f g x = equiv_class (reach f g) X x

⊢ ∀f g X x y.
    Group g ∧ (g act X) f ∧ x ∈ X ∧ y ∈ X ⇒
    (orbit f g x = orbit f g y ⇔ (x ~~ y) f g)

⊢ ∀f g x. FINITE G ⇒ FINITE (orbit f g x)

⊢ ∀f g X x. (g act X) f ∧ x ∈ X ∧ FINITE X ⇒ FINITE (orbit f g x)

⊢ ∀f g X x.
    (g act X) f ∧ x ∈ X ∧ FINITE X ∧ INJ (λa. f a x) G (orbit f g x) ⇒
    CARD (orbit f g x) = CARD G

⊢ ∀f g x a. a ∈ G ⇒ f a x ∈ orbit f g x

⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ x ∈ orbit f g x

⊢ ∀f g X x. x ∈ X ⇒ orbit f g x ∈ orbits f g X

⊢ ∀f g X.
    (g act X) f ⇒ ∀x. x ∈ X ∧ orbit f g x = {x} ⇒ x ∈ fixed_points f g X

⊢ ∀f g X x.
    Group g ∧ (g act X) f ∧ x ∈ X ⇒
    BIJ (λy. act_by f g x y * stabilizer f g x) (orbit f g x)
      {a * stabilizer f g x | a | a ∈ G}

⊢ ∀f g X x.
    Group g ∧ (g act X) f ∧ x ∈ X ⇒
    BIJ (λy. act_by f g x y * stabilizer f g x) (orbit f g x)
      (CosetPartition g (StabilizerGroup f g x))

⊢ ∀f g X x.
    Group g ∧ (g act X) f ∧ x ∈ X ⇒
    ∀a b.
      a ∈ G ∧ b ∈ G ∧ f a x = f b x ⇒
      a * stabilizer f g x = b * stabilizer f g x

⊢ ∀f g X x.
    Group g ∧ (g act X) f ∧ x ∈ X ⇒
    ∀a b.
      a ∈ G ∧ b ∈ G ∧ a * stabilizer f g x = b * stabilizer f g x ⇒
      f a x = f b x

⊢ ∀f g X x.
    FiniteGroup g ∧ (g act X) f ∧ x ∈ X ∧ FINITE X ⇒
    CARD G = CARD (orbit f g x) * CARD (stabilizer f g x)

⊢ ∀f g X x. (g act X) f ∧ x ∈ X ⇒ orbit f g x ⊆ X

⊢ ∀f g X. orbits f g X = {orbit f g x | x ∈ X}

⊢ ∀f g X e. e ∈ orbits f g X ⇔ ∃x. x ∈ X ∧ e = orbit f g x

⊢ ∀f g X e x. (g act X) f ∧ e ∈ orbits f g X ∧ x ∈ e ⇒ x ∈ X

⊢ ∀f g X. (g act X) f ∧ FINITE X ⇒ EVERY_FINITE (orbits f g X)

⊢ ∀f g X e x.
    Group g ∧ (g act X) f ∧ e ∈ orbits f g X ∧ x ∈ e ⇒ e = orbit f g x

⊢ ∀f g X. Group g ∧ (g act X) f ⇒ ∀e. e ∈ orbits f g X ⇒ e ≠ ∅

⊢ ∀f g X e. (g act X) f ∧ e ∈ orbits f g X ⇒ e ⊆ X

⊢ ∀f g X. (g act X) f ⇒ orbits f g X = partition (reach f g) X

⊢ ∀f g X n.
    Group g ∧ (g act X) f ∧ FINITE X ∧ (∀x. x ∈ X ⇒ CARD (orbit f g x) = n) ⇒
    ∀e. e ∈ orbits f g X ⇒ CARD e = n

⊢ ∀f g X n.
    Group g ∧ (g act X) f ∧ FINITE X ∧ (∀x. x ∈ X ⇒ CARD (orbit f g x) = n) ⇒
    n divides CARD X

⊢ ∀f g X. FINITE X ⇒ FINITE (orbits f g X)

⊢ ∀f g X n.
    Group g ∧ (g act X) f ∧ FINITE X ∧
    (∀x. x ∈ X ⇒ n divides CARD (orbit f g x)) ⇒
    ∀e. e ∈ orbits f g X ⇒ n divides CARD e

⊢ ∀f g X n.
    Group g ∧ (g act X) f ∧ FINITE X ∧
    (∀x. x ∈ X ⇒ n divides CARD (orbit f g x)) ⇒
    n divides CARD X

⊢ ∀g. orders g = preimage ord G

⊢ ∀f g1 g2 h.
    FiniteGroup g1 ∧ Group g2 ∧ h ≤ g2 ∧ GroupHomo f g1 g2 ∧
    SURJ f g1.carrier g2.carrier ⇒
    CARD (preimage_group f g1 g2 h.carrier).carrier =
    CARD h.carrier * CARD (kernel f g1 g2)

⊢ ∀f g1 g2 h.
    Group g1 ∧ Group g2 ∧ GroupHomo f g1 g2 ∧ h ≤ g2 ⇒
    Group (preimage_group f g1 g2 h.carrier)

⊢ ∀f g1 g2 h x. x ∈ PREIMAGE f h ∩ g1.carrier ⇒ x ∈ g1.carrier ∧ f x ∈ h

⊢ ∀f g1 g2 h.
    Group g1 ∧ Group g2 ∧ h ≤ g1 ∧ GroupHomo f g1 g2 ∧
    SURJ f g1.carrier g2.carrier ∧ kernel f g1 g2 ⊆ H ⇒
    PREIMAGE f (IMAGE f H) ∩ g1.carrier ⊆ H

⊢ ∀f g1 g2 h2.
    Group g1 ∧ Group g2 ∧ h2 ≤ g2 ∧ GroupHomo f g1 g2 ⇒
    kernel f g1 g2 ⊆ PREIMAGE f h2.carrier ∩ g1.carrier

⊢ ∀f g1 g2 h.
    Group g1 ∧ Group g2 ∧ GroupHomo f g1 g2 ∧ h ≤ g2 ⇒
    preimage_group f g1 g2 h.carrier ≤ g1

⊢ Π = OP_IMAGE (λx y. x * y) 1

⊢ ∀g h.
    h << g ⇒
    ∀x y z.
      x ∈ CosetPartition g h ∧ y ∈ CosetPartition g h ∧
      z ∈ CosetPartition g h ⇒
      (x ∘ y) ∘ z = x ∘ y ∘ z

⊢ ∀g h.
    h ≤ g ⇒
    ∀x y.
      x ∈ CosetPartition g h ∧ y ∈ CosetPartition g h ⇒
      x ∘ y ∈ CosetPartition g h

⊢ ∀g h. h << g ⇒ Group (g / h)

⊢ ∀g h.
    h << g ⇒
    H ∈ CosetPartition g h ∧ ∀x. x ∈ CosetPartition g h ⇒ H ∘ x = x

⊢ ∀g h.
    h << g ⇒
    ∀x. x ∈ CosetPartition g h ⇒ ∃y. y ∈ CosetPartition g h ∧ y ∘ x = H

⊢ ∀f g X. Group g ∧ (g act X) f ⇒ reach f g equiv_on X

⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ (x ~~ x) f g

⊢ ∀f g X x y.
    Group g ∧ (g act X) f ∧ x ∈ X ∧ y ∈ X ∧ (x ~~ y) f g ⇒ (y ~~ x) f g

⊢ ∀f g X x y z.
    Group g ∧ (g act X) f ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X ∧ (x ~~ y) f g ∧
    (y ~~ z) f g ⇒
    (x ~~ z) f g

⊢ ∀g X a. X * a = {z * a | z ∈ X}

⊢ ∀g. (uroots 0).carrier = G

⊢ ∀g n x. x ∈ (uroots n).carrier ⇔ x ∈ G ∧ x ** n = #e

⊢ ∀g n. (uroots n).carrier ⊆ G

⊢ ∀f g X.
    Group g ∧ (g act X) f ∧ FINITE X ⇒
    CARD (sing_orbits f g X) = CARD (fixed_points f g X)

⊢ ∀f g X e. e ∈ sing_orbits f g X ⇔ e ∈ orbits f g X ∧ SING e

⊢ ∀f g X e. e ∈ sing_orbits f g X ⇒ CARD e = 1

⊢ ∀f g X.
    Group g ∧ (g act X) f ⇒
    ∀e. e ∈ sing_orbits f g X ⇒ CHOICE e ∈ fixed_points f g X

⊢ ∀f g X e. e ∈ sing_orbits f g X ⇒ FINITE e

⊢ ∀f g X e. (g act X) f ∧ e ∈ sing_orbits f g X ⇒ e ⊆ X

⊢ ∀f g X. FINITE X ⇒ FINITE (sing_orbits f g X)

⊢ ∀f g X. sing_orbits f g X ⊆ orbits f g X

⊢ ∀f g X.
    Group g ∧ (g act X) f ⇒
    BIJ (λe. CHOICE e) (sing_orbits f g X) (fixed_points f g X)

⊢ ∀f g X.
    Group g ∧ (g act X) f ⇒
    INJ (λe. CHOICE e) (sing_orbits f g X) (fixed_points f g X)

⊢ ∀f g X.
    Group g ∧ (g act X) f ⇒
    SURJ (λe. CHOICE e) (sing_orbits f g X) (fixed_points f g X)

⊢ ∀f g X x.
    Group g ∧ (g act X) f ∧ x ∈ X ⇒
    stabilizer f g x = IMAGE (λa. if f a x = x then a else #e) G

⊢ ∀f g X x a.
    Group g ∧ (g act X) f ∧ x ∈ X ∧ a ∈ G ⇒
    conjugate g a (stabilizer f g x) = stabilizer f g (f a x)

⊢ ∀f g x a. a ∈ stabilizer f g x ⇔ a ∈ G ∧ f a x = x

⊢ ∀f g X x.
    FiniteGroup g ∧ (g act X) f ∧ x ∈ X ⇒
    CARD (stabilizer f g x) divides CARD G

⊢ ∀f g x. (StabilizerGroup f g x).carrier = stabilizer f g x

⊢ ∀f g X x.
    FiniteGroup g ∧ (g act X) f ∧ x ∈ X ⇒
    FiniteGroup (StabilizerGroup f g x)

⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ Group (StabilizerGroup f g x)

⊢ ∀f g x. (StabilizerGroup f g x).id = #e

⊢ ∀f g x.
    (StabilizerGroup f g x).carrier = stabilizer f g x ∧
    (StabilizerGroup f g x).op = $* ∧ (StabilizerGroup f g x).id = #e

⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ StabilizerGroup f g x ≤ g

⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ #e ∈ stabilizer f g x

⊢ ∀f g X x. Group g ∧ (g act X) f ∧ x ∈ X ⇒ stabilizer f g x ≠ ∅

⊢ ∀f g x. stabilizer f g x ⊆ G

⊢ ∀g h. subgroup h g ∧ subgroup g h ⇒ GroupIso I h g

⊢ ∀g. Group g ⇒
      ∀h. h ≤ g ⇔
          H ≠ ∅ ∧ H ⊆ G ∧ $o = $* ∧ #i = #e ∧
          ∀x y. x ∈ H ∧ y ∈ H ⇒ x * |/ y ∈ H

⊢ ∀g h. h ≤ g ∧ g ≤ h ⇒ h = g

⊢ ∀g. sgbcross ∅ = gen #e

⊢ ∀g. FiniteAbelianGroup g ⇒
      ∀B. B ⊆ all_subgroups g ⇒
          ∀h. h ∈ all_subgroups g ∧ h ∉ B ⇒
              sgbcross (h INSERT B) = h ∘ sgbcross B

⊢ ∀g. FiniteAbelianGroup g ⇒
      ∀B. B ⊆ all_subgroups g ⇒
          ∀h. h ∈ all_subgroups g ⇒
              sgbcross (h INSERT B) = h ∘ sgbcross (B DELETE h)

⊢ ∀g x. x ∈ (sgbINTER g).carrier ⇔ ∀h. h ≤ g ⇒ x ∈ H

⊢ ∀g. Group g ⇒ Group (sgbINTER g)

⊢ ∀g. (sgbINTER g).id ∈ (sgbINTER g).carrier

⊢ ∀g x. x ∈ (sgbINTER g).carrier ⇒ |/ x ∈ (sgbINTER g).carrier

⊢ ∀g x y.
    x ∈ (sgbINTER g).carrier ∧ y ∈ (sgbINTER g).carrier ⇒
    (sgbINTER g).op x y ∈ (sgbINTER g).carrier

⊢ ∀g. (sgbINTER g).carrier = BIGINTER (IMAGE (λh. H) {h | h ≤ g}) ∧
      (∀x y.
         x ∈ (sgbINTER g).carrier ∧ y ∈ (sgbINTER g).carrier ⇒
         (sgbINTER g).op x y = x * y) ∧ (sgbINTER g).id = #e

⊢ ∀g. Group g ⇒ sgbINTER g ≤ g

⊢ ∀g. Group g ⇒ (sgbINTER g).carrier ⊆ G

⊢ ∀g h. subgroup h g ∧ G ⊆ H ⇒ GroupIso I h g

⊢ ∀g h. h ≤ g ⇒ H ≠ ∅

⊢ ∀g h. h ≤ g ⇒ H ⊆ G

⊢ ∀g h.
    h ≤ g ⇒
    ∀a. a ∈ G ⇒ BIJ (λz. a * z * |/ a) H (conjugate_subgroup h g a).carrier

⊢ ∀g h. h ≤ g ∧ FINITE H ⇒ ∀a. a ∈ G ⇒ CARD (a * H) = CARD H

⊢ ∀g h.
    h ≤ g ∧ FINITE G ⇒
    ∀e. e ∈ partition (left_coset g H) G ⇒ CARD e = CARD H

⊢ ∀g h. h ≤ g ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ (x * H = y * H ⇔ |/ y * x ∈ H)

⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ IMAGE (left_coset g H) G ⇔ x ∈ CosetPartition g h

⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ G ⇒ x ∈ x * H

⊢ ∀g h.
    h ≤ g ⇒ ∀e. e ∈ partition (left_coset g H) G ⇔ ∃a. a ∈ G ∧ e = a * H

⊢ ∀g h a x. h ≤ g ∧ a ∈ G ∧ x ∈ a * H ⇒ x ∈ G

⊢ ∀g h. h ≤ g ⇒ ∀a b. a ∈ G ∧ b ∈ G ∧ b ∈ a * H ⇒ a ∈ b * H

⊢ ∀g h.
    h ≤ g ⇒
    ∀a b c. a ∈ G ∧ b ∈ G ∧ c ∈ G ∧ b ∈ a * H ∧ c ∈ b * H ⇒ c ∈ a * H

⊢ ∀g h1 h2 h3. h1 ≤ g ∧ h2 ≤ g ∧ h3 ≤ g ⇒ (h1 ∘ h2) ∘ h3 = h1 ∘ h2 ∘ h3

⊢ ∀g h1 h2.
    h1 ≤ g ∧ h2 ≤ g ∧ FINITE G ⇒
    (let
       s1 = h1.carrier;
       s2 = h2.carrier
     in
       CARD (h1 ∘ h2).carrier = CARD s1 * CARD s2 DIV CARD (s1 ∩ s2))

⊢ ∀g h1 h2.
    h1 ≤ g ∧ h2 ≤ g ∧ FINITE G ⇒
    (let
       s1 = h1.carrier;
       s2 = h2.carrier
     in
       CARD (h1 ∘ h2).carrier * CARD (s1 ∩ s2) = CARD s1 * CARD s2)

⊢ ∀g. AbelianGroup g ⇒ closure_comm_assoc_fun $o (all_subgroups g)

⊢ ∀g. AbelianGroup g ⇒ ∀h1 h2. h1 ≤ g ∧ h2 ≤ g ⇒ h1 ∘ h2 = h2 ∘ h1

⊢ ∀g h1 h2.
    h1 ≤ g ∧ h2 ≤ g ∧ h1 ∘ h2 = h2 ∘ h1 ∧ FiniteGroup h1 ∧ FiniteGroup h2 ⇒
    FiniteGroup (h1 ∘ h2)

⊢ ∀g h1 h2. h1 ≤ g ∧ h2 ≤ g ∧ h1 ∘ h2 = h2 ∘ h1 ⇒ Group (h1 ∘ h2)

⊢ ∀g h1 h2.
    (h1 ∘ h2).carrier = h1.carrier ∘ h2.carrier ∧ (h1 ∘ h2).op = $* ∧
    (h1 ∘ h2).id = #e

⊢ ∀g h. h ≤ g ⇒ h ∘ h = h

⊢ ∀g h1 h2. h1 ≤ g ∧ h2 ≤ g ∧ h1 ∘ h2 = h2 ∘ h1 ⇒ h1 ∘ h2 ≤ g

⊢ ∀g h. h ≤ g ⇒ ∀z. z ∈ H ⇒ z ∈ G

⊢ ∀g h1 h2. h1 ≤ g ∧ h2 ≤ g ⇒ (h1 = h2 ⇔ h1.carrier = h2.carrier)

⊢ ∀g h. h ≤ g ∧ H = G ⇒ h = g

⊢ ∀g h. subgroup h g ⇔ H ⊆ G ∧ ∀x y. x ∈ H ∧ y ∈ H ⇒ x ∘ y = x * y

⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ H ⇒ ∀n. h.exp x n = x ** n

⊢ ∀g h. h ≤ g ⇒ Group h ∧ Group g

⊢ ∀g h. h ≤ g ⇒ Group g ∧ Group h

⊢ ∀g h k f. subgroup h g ∧ GroupHomo f g k ⇒ GroupHomo f h k

⊢ ∀g h. h ≤ g ⇒ Group h ∧ Group g ∧ subgroup h g

⊢ ∀g h. h ≤ g ⇒ #i = #e

⊢ ∀g h. h ≤ g ⇒ left_coset g H equiv_on G

⊢ ∀g h k. h ≤ g ∧ k ≤ g ⇒ Group (h mINTER k)

⊢ ∀g h k. h ≤ g ∧ k ≤ g ⇒ ∀x. x ∈ H ∩ K ⇒ |/ x ∈ H ∩ K

⊢ ∀g h k. h ≤ g ∧ k ≤ g ⇒ ∀x. x ∈ H ∩ K ⇒ (h mINTER k).inv x = |/ x

⊢ ∀g h k.
    h ≤ g ∧ k ≤ g ⇒
    (h mINTER k).carrier = H ∩ K ∧
    (∀x y. x ∈ H ∩ K ∧ y ∈ H ∩ K ⇒ (h mINTER k).op x y = x * y) ∧
    (h mINTER k).id = #e ∧ ∀x. x ∈ H ∩ K ⇒ (h mINTER k).inv x = |/ x

⊢ ∀g h k. h ≤ g ∧ k ≤ g ⇒ (h mINTER k) ≤ g

⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ H ⇒ h.inv x = |/ x

⊢ ∀g h. h ≤ g ⇒ ∀x y. x ∈ H ∧ y ∈ H ⇒ x * |/ y ∈ H

⊢ ∀g h. h ≤ g ⇒ Group h

⊢ ∀g h. h ≤ g ⇒ h << g

⊢ ∀g h. Group g ∧ Group h ∧ subgroup h g ⇒ submonoid h g

⊢ ∀g h. h ≤ g ⇒ $o = $*

⊢ ∀g h. h ≤ g ⇒ ∀x. x ∈ H ⇒ order h x = ord x

⊢ ∀g h. Group g ∧ Group h ∧ subgroup h g ⇒ ∀x. x ∈ H ⇒ order h x = ord x

⊢ ∀g h. h ≤ g ⇒ Group h ∧ Group g ∧ ∀x y. x ∈ H ∧ y ∈ H ⇒ x ∘ y = x * y

⊢ ∀g h.
    h ≤ g ⇒
    Group g ∧ Group h ∧ H ≠ ∅ ∧ H ⊆ G ∧ $o = $* ∧ #i = #e ∧
    (∀x. x ∈ H ⇒ h.inv x = |/ x) ∧ ∀x y. x ∈ H ∧ y ∈ H ⇒ x * |/ y ∈ H

⊢ ∀g. Group g ⇒ g ≤ g

⊢ ∀g. subgroup g g

⊢ ∀g h. subgroup h g ⇒ H ⊆ G

⊢ ∀g. Group g ⇒ ∀h. h ≤ g ⇔ H ≠ ∅ ∧ H ⊆ G ∧ h ∘ h = h ∧ IMAGE |/ H = H

⊢ ∀g h.
    h ≤ g ⇔
    Group g ∧ $o = $* ∧ #i = #e ∧ H ≠ ∅ ∧ H ⊆ G ∧
    ∀x y. x ∈ H ∧ y ∈ H ⇒ x * |/ y ∈ H

⊢ ∀g h. h ≤ g ⇒ ∀a. a ∈ G ⇒ BIJ (λx. a * x) H (a * H)

⊢ ∀g h t. h ≤ t ∧ t ≤ g ⇒ h ≤ g

⊢ ∀g h k. subgroup g h ∧ subgroup h k ⇒ subgroup g k

⊢ ∀g. ssbcross ∅ = {#e}

⊢ ∀g. FiniteAbelianGroup g ⇒
      ∀B. B ⊆ POW G ⇒
          ∀s. s ⊆ G ∧ s ∉ B ⇒ ssbcross (s INSERT B) = s ∘ ssbcross B

⊢ ∀g. FiniteAbelianGroup g ⇒
      ∀B. B ⊆ POW G ⇒
          ∀s. s ⊆ G ⇒ ssbcross (s INSERT B) = s ∘ ssbcross (B DELETE s)

⊢ ∀g s1 s2. s1 ∘ s2 = IMAGE (λ(x,y). x * y) (s1 × s2)

⊢ ∀g. Group g ⇒
      ∀s1 s2 s3. s1 ⊆ G ∧ s2 ⊆ G ∧ s3 ⊆ G ⇒ (s1 ∘ s2) ∘ s3 = s1 ∘ s2 ∘ s3

⊢ ∀g. AbelianGroup g ⇒ closure_comm_assoc_fun $o (POW G)

⊢ ∀g. AbelianGroup g ⇒ ∀s1 s2. s1 ⊆ G ∧ s2 ⊆ G ⇒ s1 ∘ s2 = s2 ∘ s1

⊢ ∀g s1 s2 x y. x ∈ s1 ∧ y ∈ s2 ⇒ x * y ∈ s1 ∘ s2

⊢ ∀g s1 s2 z. z ∈ s1 ∘ s2 ⇔ ∃x y. x ∈ s1 ∧ y ∈ s2 ∧ z = x * y

⊢ ∀g h1 h2.
    h1 ≤ g ∧ h2 ≤ g ∧ FINITE G ⇒
    (let
       s1 = h1.carrier;
       s2 = h2.carrier;
       f (x,y) = x * y
     in
       ∀z. z ∈ s1 ∘ s2 ⇒ CARD (preimage f (s1 × s2) z) = CARD (s1 ∩ s2))

⊢ ∀g s1 s2. FINITE s1 ∧ FINITE s2 ⇒ FINITE (s1 ∘ s2)

⊢ ∀g. Group g ⇒
      ∀s1 s2.
        s1 ⊆ G ∧ s2 ⊆ G ⇒ IMAGE |/ (s1 ∘ s2) = IMAGE |/ s2 ∘ IMAGE |/ s1

⊢ ∀g h1 h2.
    h1 ≤ g ∧ h2 ≤ g ∧ FINITE G ⇒
    (let
       s1 = h1.carrier;
       s2 = h2.carrier;
       f (x,y) = x * y
     in
       ∀t. t ∈ partition (feq f) (s1 × s2) ⇒ CARD t = CARD (s1 ∩ s2))

⊢ ∀g s1 s2.
    INJ (preimage (λ(x,y). x * y) (s1 × s2)) (s1 ∘ s2) 𝕌(:α # α -> bool)

⊢ ∀g h. h ≤ g ⇒ H ∘ H = H

⊢ ∀g. Group g ⇒ ∀s1 s2. s1 ⊆ G ∧ s2 ⊆ G ⇒ s1 ∘ s2 ⊆ G

⊢ ∀g h1 h2.
    h1 ≤ g ∧ h2 ≤ g ⇒
    (let
       s1 = h1.carrier;
       s2 = h2.carrier;
       f (x,y) = x * y
     in
       ∀z. z ∈ s1 ∘ s2 ⇒
           BIJ (λd. (left z * d,|/ d * right z)) (s1 ∩ s2)
             (preimage f (s1 × s2) z))

⊢ ∀g s x. x ∈ s ⇒ ∀n. (subset_group g s).exp x n = x ** n

⊢ ∀g s x. x ∈ s ⇒ order (subset_group g s) x = ord x

⊢ ∀g s.
    (subset_group g s).carrier = s ∧ (subset_group g s).op = $* ∧
    (subset_group g s).id = #e

⊢ ∀g s.
    Group g ∧ s ≠ ∅ ∧ s ⊆ G ∧ (∀x y. x ∈ s ∧ y ∈ s ⇒ x * |/ y ∈ s) ⇒
    subset_group g s ≤ g

⊢ ∀g s.
    Monoid g ∧ #e ∈ s ∧ s ⊆ G ∧ (∀x y. x ∈ s ∧ y ∈ s ⇒ x * y ∈ s) ⇒
    subset_group g s << g

⊢ ∀f g1 g2 h.
    Group g1 ∧ Group g2 ∧ h ≤ g1 ∧ GroupHomo f g1 g2 ⇒
    H ⊆ PREIMAGE f (IMAGE f H) ∩ g1.carrier

⊢ ∑ = OP_IMAGE (λx y. x + y) 0

⊢ AbelianGroup symdiff_set

⊢ Group symdiff_set

⊢ ∀f g X n.
    Group g ∧ (g act X) f ∧ FINITE X ∧ 0 < n ∧
    (∀e. e ∈ multi_orbits f g X ⇒ CARD e = n) ⇒
    CARD X MOD n = CARD (fixed_points f g X) MOD n

⊢ ∀f g X.
    Group g ∧ (g act X) f ∧ FINITE X ⇒
    CARD X = CARD (fixed_points f g X) + ∑ CARD (multi_orbits f g X)

⊢ ∀f g X.
    Group g ∧ (g act X) f ∧ FINITE X ⇒
    CARD X = CARD (sing_orbits f g X) + ∑ CARD (multi_orbits f g X)

⊢ ∀f g X. Group g ∧ (g act X) f ∧ FINITE X ⇒ CARD X = ∑ CARD (orbits f g X)

⊢ ∀f g X. DISJOINT (sing_orbits f g X) (multi_orbits f g X)

⊢ ∀f g X. orbits f g X = sing_orbits f g X ∪ multi_orbits f g X

⊢ ∀e. FiniteAbelianGroup (trivial_group e)

⊢ ∀e. (trivial_group e).carrier = {e}

⊢ ∀e. (trivial_group e).id = e