Theory monoid

⊢ ∀g. AbelianMonoid g ⇔ Monoid g ∧ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x

⊢ ∀g. FiniteAbelianMonoid g ⇔ AbelianMonoid g ∧ FINITE G

⊢ ∀g. FiniteMonoid g ⇔ Monoid g ∧ FINITE G

⊢ ∀g s. GPROD_SET g s = GITSET g s #e

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

⊢ ∀f g. MonoidAuto f g ⇔ MonoidIso f g g

⊢ ∀f g. MonoidEndo f g ⇔ MonoidHomo f g g

⊢ ∀f g h.
    MonoidHomo 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 #e = h.id

⊢ ∀f g h. MonoidIso f g h ⇔ MonoidHomo f g h ∧ BIJ f G h.carrier

⊢ ∀g. Monoid 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 * #e = x

⊢ ∀h g. h << g ⇔ Monoid h ∧ Monoid g ∧ H ⊆ G ∧ $o = $* ∧ #i = #e

⊢ ∀f g h.
    WeakHomo 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. WeakIso f g h ⇔ WeakHomo f g h ∧ BIJ f G h.carrier

⊢ addition_monoid = <|carrier := 𝕌(:num); op := $+; id := 0|>

⊢ ∀m. extend m =
      <|carrier := 𝕌(:α); id := m.id;
        op :=
          (λx y.
               if x ∈ m.carrier then if y ∈ m.carrier then m.op x y else y
               else x)|>

⊢ ∀g f.
    homo_monoid g f =
    <|carrier := IMAGE f G; op := image_op g f; id := f #e|>

⊢ ∀g f x y.
    image_op g f x y =
    f (CHOICE (preimage f G x) * CHOICE (preimage f G y))

⊢ lists = <|carrier := 𝕌(:α list); id := []; op := $++ |>

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('monoid').
             (∀a0'.
                (∃a0 a1 a2.
                   a0' =
                   (λa0 a1 a2.
                        ind_type$CONSTR 0 (a0,a1,a2) (λn. ind_type$BOTTOM))
                     a0 a1 a2) ⇒
                $var$('monoid') a0') ⇒
             $var$('monoid') a0') rep

⊢ ∀a0 a1 a2 f. monoid_CASE (monoid a0 a1 a2) f = f a0 a1 a2

⊢ ∀g x n. x ** n = FUNPOW ($* x) n #e

⊢ ∀g f.
    monoid_inj_image g f =
    <|carrier := IMAGE f G;
      op := (let t = LINV f G in λx y. f (t x * t y)); id := f #e|>

⊢ ∀g h. (g mINTER h) = <|carrier := G ∩ H; op := $*; id := #e|>

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

⊢ ∀g. G* = {x | x ∈ G ∧ ∃y. y ∈ G ∧ x * y = #e ∧ y * x = #e}

⊢ ∀f a0 a1 a2. monoid_size f (monoid a0 a1 a2) = 1 + f a2

⊢ multiplication_monoid = <|carrier := 𝕌(:num); op := $*; id := 1|>

⊢ ∀g x. ord x = case OLEAST k. period g x k of NONE => 0 | SOME k => k

⊢ ∀g n. orders g n = {x | x ∈ G ∧ ord x = n}

⊢ ∀g x k. period g x k ⇔ 0 < k ∧ x ** k = #e

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

⊢ ∀b. power_monoid b =
      <|carrier := {b ** j | j ∈ 𝕌(:num)}; op := $*; id := 1|>

⊢ ∀f f0 a. (monoid f f0 a).carrier = f

⊢ ∀f1 f f0 a. monoid f f0 a with carrier updated_by f1 = monoid (f1 f) f0 a

⊢ ∀f f0 a. (monoid f f0 a).id = a

⊢ ∀f1 f f0 a. monoid f f0 a with id updated_by f1 = monoid f f0 (f1 a)

⊢ ∀f f0 a. (monoid f f0 a).op = f0

⊢ ∀f1 f f0 a. monoid f f0 a with op updated_by f1 = monoid f (f1 f0) a

⊢ set_inter = <|carrier := 𝕌(:α -> bool); id := 𝕌(:α); op := $INTER|>

⊢ set_union = <|carrier := 𝕌(:α -> bool); id := ∅; op := $UNION|>

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

⊢ ∀h g. submonoid h g ⇔ MonoidHomo I h g

⊢ ∀n. times_mod n =
      <|carrier := count n; id := if n = 1 then 0 else 1;
        op := (λi j. i * j MOD n)|>

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

⊢ ∀g b.
    AbelianMonoid g ∧ FINITE_BAG b ∧ SET_OF_BAG b ⊆ G ⇒
    ∀x a::G. GITBAG g (BAG_INSERT x b) a = GITBAG g b (x * a)

⊢ ∀g s.
    AbelianMonoid g ∧ FINITE s ∧ s ⊆ G ⇒
    ∀b x::G. GITSET g (x INSERT s) b = GITSET g (s DELETE x) (x * b)

⊢ ∀g s.
    AbelianMonoid g ∧ FINITE s ∧ s ⊆ G ⇒
    ∀b x::G. GITSET g (x INSERT s) b = x * GITSET g (s DELETE x) b

⊢ ∀g s.
    AbelianMonoid g ∧ FINITE s ∧ s ⊆ G ⇒
    ∀b x::G. GITSET g s (x * b) = x * GITSET g s b

⊢ ∀P. (∃m. P m) ⇔ ∃f0 f a. P <|carrier := f0; op := f; id := a|>

⊢ ∀P. (∀m. P m) ⇔ ∀f0 f a. P <|carrier := f0; op := f; id := a|>

⊢ ∀g. FiniteAbelianMonoid g ⇔
      FiniteMonoid g ∧ ∀x y. x ∈ G ∧ y ∈ G ⇒ x * y = y * x

⊢ AbelianMonoid g ⇒
  ∀b. FINITE_BAG b ⇒
      IMAGE f (SET_OF_BAG b ∩ P) ⊆ G ⇒
      GBAG g (BAG_IMAGE f (BAG_FILTER P b)) =
      GBAG g (BAG_IMAGE (λx. if P x then f x else #e) b)

⊢ AbelianMonoid g ∧ FINITE s ⇒
  ∀b. FINITE_BAG b ⇒
      IMAGE f (SET_OF_BAG b) ⊆ G ∧ (∀x. x ⋲ b ⇒ ∃P. P ∈ s ∧ P x) ∧
      (∀x P1 P2. x ⋲ b ∧ P1 ∈ s ∧ P2 ∈ s ∧ P1 x ∧ P2 x ⇒ P1 = P2) ⇒
      GBAG g
        (BAG_IMAGE (λP. GBAG g (BAG_IMAGE f (BAG_FILTER P b)))
           (BAG_OF_SET s)) =
      GBAG g (BAG_IMAGE f b)

⊢ AbelianMonoid g ∧ FINITE_BAG b ∧ SET_OF_BAG b ⊆ G ∧ x ∈ G ⇒
  GBAG g (BAG_INSERT x b) = x * GBAG g b

⊢ AbelianMonoid g ∧ FINITE s ∧ FINITE_BAG b ∧ SET_OF_BAG b ⊆ G ∧
  (∀x. x ⋲ b ⇒ ∃P. P ∈ s ∧ P x) ∧
  (∀x P1 P2. x ⋲ b ∧ P1 ∈ s ∧ P2 ∈ s ∧ P1 x ∧ P2 x ⇒ P1 = P2) ⇒
  GBAG g (BAG_IMAGE (λP. GBAG g (BAG_FILTER P b)) (BAG_OF_SET s)) =
  GBAG g b

⊢ AbelianMonoid g ∧ FINITE_BAG b1 ∧ FINITE_BAG b2 ∧ SET_OF_BAG b1 ⊆ G ∧
  SET_OF_BAG b2 ⊆ G ⇒
  GBAG g (b1 ⊎ b2) = GBAG g b1 * GBAG g b2

⊢ ∀g b. AbelianMonoid g ∧ FINITE_BAG b ∧ SET_OF_BAG b ⊆ G ⇒ GBAG g b ∈ G

⊢ ∀g. AbelianMonoid g ⇒
      ∀b. FINITE_BAG b ⇒
          ∀p q a.
            IMAGE p (SET_OF_BAG b) ⊆ G ∧ IMAGE q (SET_OF_BAG b) ⊆ G ∧ a ∈ G ⇒
            GITBAG g (BAG_IMAGE (λx. p x * q x) b) a =
            GITBAG g (BAG_IMAGE p b) a * GBAG g (BAG_IMAGE q b)

⊢ ∀g. AbelianMonoid g ⇒
      ∀b. FINITE_BAG b ⇒
          ∀b' a a'.
            FINITE_BAG b' ∧ a ∈ G ∧ SET_OF_BAG b ⊆ G ∧ SET_OF_BAG b' ⊆ G ∧
            (∀x. x ⋲ b ⊎ b' ∧ x ≠ #e ⇒ b x = b' x) ⇒
            GITBAG g b a = GITBAG g b' a

⊢ ∀g a. GITBAG g {||} a = a

⊢ ∀g. AbelianMonoid g ⇒
      ∀b. FINITE_BAG b ⇒
          ∀a. a ∈ G ∧ SET_OF_BAG b ⊆ G ⇒ GITBAG g b a = a * GBAG g b

⊢ ∀b. FINITE_BAG b ⇒
      ∀g x a.
        GITBAG g (BAG_INSERT x b) a =
        GITBAG g (BAG_REST (BAG_INSERT x b))
          (BAG_CHOICE (BAG_INSERT x b) * a)

⊢ ∀g b x a.
    (AbelianMonoid g ∧ FINITE_BAG b ∧ SET_OF_BAG b ⊆ G) ∧ x ∈ G ∧ a ∈ G ⇒
    GITBAG g (BAG_INSERT x b) a = GITBAG g b (x * a)

⊢ ∀g b acc.
    FINITE_BAG b ⇒
    GITBAG g b acc =
    if b = {||} then acc else GITBAG g (BAG_REST b) (BAG_CHOICE b * acc)

⊢ ∀g. AbelianMonoid g ⇒
      ∀b1.
        FINITE_BAG b1 ⇒
        ∀b2.
          FINITE_BAG b2 ∧ SET_OF_BAG b1 ⊆ G ∧ SET_OF_BAG b2 ⊆ G ⇒
          ∀a. a ∈ G ⇒ GITBAG g (b1 ⊎ b2) a = GITBAG g b2 (GITBAG g b1 a)

⊢ ∀g. AbelianMonoid g ⇒
      ∀b. FINITE_BAG b ⇒ ∀a. SET_OF_BAG b ⊆ G ∧ a ∈ G ⇒ GITBAG g b a ∈ G

⊢ g1.op = g2.op ⇒ ∀b. FINITE_BAG b ⇒ ∀a. GITBAG g1 b a = GITBAG g2 b a

⊢ ∀g b. GITSET g ∅ b = b

⊢ ∀s. FINITE s ⇒
      ∀x g b.
        GITSET g (x INSERT s) b =
        GITSET g (REST (x INSERT s)) (CHOICE (x INSERT s) * b)

⊢ ∀g s.
    FINITE s ∧ s ≠ ∅ ⇒ ∀b. GITSET g s b = GITSET g (REST s) (CHOICE s * b)

⊢ ∀s g b.
    FINITE s ⇒
    GITSET g s b = if s = ∅ then b else GITSET g (REST s) (CHOICE s * b)

⊢ ∀g s. GPROD_SET g ∅ = #e

⊢ ∀g s. AbelianMonoid g ∧ FINITE s ∧ s ⊆ G ⇒ GPROD_SET g s ∈ G

⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G ⇒ GPROD_SET g {x} = x

⊢ ∀g s.
    GPROD_SET g ∅ = #e ∧
    (AbelianMonoid g ∧ FINITE s ∧ s ⊆ G ⇒
     ∀x::G. GPROD_SET g (x INSERT s) = x * GPROD_SET g (s DELETE x))

⊢ AbelianMonoid g ∧ x ∈ G ∧ SET_OF_BAG b ⊆ {x} ⇒ GBAG g b = x ** b x

⊢ AbelianMonoid g ⇒ ∀b. BAG_EVERY ($= #e) b ⇒ GBAG g b = #e

⊢ ∀g. (Invertibles g).carrier = G*

⊢ ∀g x. order (Invertibles g) x = ord x

⊢ ∀g. (Invertibles g).carrier = G* ∧ (Invertibles g).op = $* ∧
      (Invertibles g).id = #e ∧ (Invertibles g).exp = $**

⊢ ∀g. (Invertibles g).carrier ⊆ G

⊢ AbelianMonoid g ∧ AbelianMonoid h ∧ MonoidHomo f g h ∧ FINITE_BAG b ∧
  SET_OF_BAG b ⊆ G ⇒
  f (GBAG g b) = GBAG h (BAG_IMAGE f b)

⊢ ∀f b t.
    SET_OF_BAG b ⊆ t ∧ closure_comm_assoc_fun f t ∧ FINITE_BAG b ⇒
    ∀x a::t. ITBAG f (BAG_INSERT x b) a = ITBAG f b (f x a)

⊢ ∀g. AbelianMonoid g ⇒ closure_comm_assoc_fun $* G

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

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

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

⊢ AbelianMonoid addition_monoid

⊢ Monoid addition_monoid

⊢ addition_monoid.carrier = 𝕌(:num) ∧ addition_monoid.op = $+ ∧
  addition_monoid.id = 0

⊢ DATATYPE (record monoid carrier op id)

⊢ (extend m).carrier = 𝕌(:α)

⊢ (extend m).id = m.id

⊢ ∀m. Monoid m ⇒ Monoid (extend m)

⊢ x ∈ m.carrier ∧ y ∈ m.carrier ⇒ (extend m).op x y = m.op x y

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

⊢ ∀g. MonoidIso I (homo_monoid g I) g

⊢ ∀g f.
    AbelianMonoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
    AbelianMonoid (homo_monoid g f)

⊢ ∀g f.
    Monoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
    ∀x y z. x ∈ fG ∧ y ∈ fG ∧ z ∈ fG ⇒ (x ∘ y) ∘ z = x ∘ y ∘ z

⊢ ∀g f. Monoid g ∧ INJ f G 𝕌(:β) ⇒ MonoidHomo f g (homo_monoid g f)

⊢ ∀g f.
    Monoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
    ∀x y. x ∈ fG ∧ y ∈ fG ⇒ x ∘ y ∈ fG

⊢ ∀g f.
    AbelianMonoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
    ∀x y. x ∈ fG ∧ y ∈ fG ⇒ x ∘ y = y ∘ x

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

⊢ ∀g f. f #e = #i

⊢ ∀g f.
    Monoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒
    #i ∈ fG ∧ ∀x. x ∈ fG ⇒ #i ∘ x = x ∧ x ∘ #i = x

⊢ ∀g f.
    Monoid g ∧ MonoidHomo f g (homo_monoid g f) ⇒ Monoid (homo_monoid g f)

⊢ ∀g f. INJ f G 𝕌(:β) ⇒ ∀x y. x ∈ G ∧ y ∈ G ⇒ f (x * y) = f x ∘ f y

⊢ ∀g f.
    fG = IMAGE f G ∧
    (∀x y.
       x ∈ fG ∧ y ∈ fG ⇒
       x ∘ y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y))) ∧
    #i = f #e

⊢ ∀g f.
    INJ f G 𝕌(:β) ⇒
    ∀x y. x ∈ G ∧ y ∈ G ⇒ image_op g f (f x) (f y) = f (x * y)

⊢ Monoid lists

⊢ ∀g. maximal_order g = MAX_SET {ord z | z | z ∈ G}

⊢ ∀a0 a1 a2 a0' a1' a2'.
    monoid a0 a1 a2 = monoid a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'

⊢ ∀f. ∃fn. ∀a0 a1 a2. fn (monoid a0 a1 a2) = f a0 a1 a2

⊢ (∀f f0 a. (monoid f f0 a).carrier = f) ∧
  (∀f f0 a. (monoid f f0 a).op = f0) ∧ ∀f f0 a. (monoid f f0 a).id = a

⊢ (∀m f. (m with op updated_by f).carrier = m.carrier) ∧
  (∀m f. (m with id updated_by f).carrier = m.carrier) ∧
  (∀m f. (m with carrier updated_by f).op = m.op) ∧
  (∀m f. (m with id updated_by f).op = m.op) ∧
  (∀m f. (m with carrier updated_by f).id = m.id) ∧
  (∀m f. (m with op updated_by f).id = m.id) ∧
  (∀m f. (m with carrier updated_by f).carrier = f m.carrier) ∧
  (∀m f. (m with op updated_by f).op = f m.op) ∧
  ∀m f. (m with id updated_by f).id = f m.id

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

⊢ ∀g. MonoidAuto I g

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

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

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

⊢ ∀f g. Monoid g ∧ MonoidAuto f g ⇒ ∀x. x ∈ G ⇒ ∀n. f (x ** n) = f x ** n

⊢ ∀f g. MonoidAuto f g ⇒ f #e = #e

⊢ ∀g f. Monoid g ∧ MonoidAuto f g ⇒ MonoidAuto (LINV f G) g

⊢ ∀g f. Monoid g ∧ MonoidAuto f g ⇒ ∀x. x ∈ G ⇒ ord (f x) = ord x

⊢ ∀g. Monoid g ⇒ G ≠ ∅

⊢ ∀M M' f.
    M = M' ∧ (∀a0 a1 a2. M' = monoid a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
    monoid_CASE M f = monoid_CASE M' f'

⊢ monoid_CASE x f = v ⇔ ∃f' f0 a. x = monoid f' f0 a ∧ f f' f0 a = v

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

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

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

⊢ ∀m1 m2. m1 = m2 ⇔ m1.carrier = m2.carrier ∧ m1.op = m2.op ∧ m1.id = m2.id

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

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

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

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

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

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

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

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

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

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

⊢ (∀f1 f f0 a.
     monoid f f0 a with carrier updated_by f1 = monoid (f1 f) f0 a) ∧
  (∀f1 f f0 a. monoid f f0 a with op updated_by f1 = monoid f (f1 f0) a) ∧
  ∀f1 f f0 a. monoid f f0 a with id updated_by f1 = monoid f f0 (f1 a)

⊢ (∀m g f.
     m with <|op updated_by f; carrier updated_by g|> =
     m with <|carrier updated_by g; op updated_by f|>) ∧
  (∀m g f.
     m with <|id updated_by f; carrier updated_by g|> =
     m with <|carrier updated_by g; id updated_by f|>) ∧
  ∀m g f.
    m with <|id updated_by f; op updated_by g|> =
    m with <|op updated_by g; id updated_by f|>

⊢ ((∀g f. op_fupd f ∘ carrier_fupd g = carrier_fupd g ∘ op_fupd f) ∧
   ∀h g f. op_fupd f ∘ carrier_fupd g ∘ h = carrier_fupd g ∘ op_fupd f ∘ h) ∧
  ((∀g f. id_fupd f ∘ carrier_fupd g = carrier_fupd g ∘ id_fupd f) ∧
   ∀h g f. id_fupd f ∘ carrier_fupd g ∘ h = carrier_fupd g ∘ id_fupd f ∘ h) ∧
  (∀g f. id_fupd f ∘ op_fupd g = op_fupd g ∘ id_fupd f) ∧
  ∀h g f. id_fupd f ∘ op_fupd g ∘ h = op_fupd g ∘ id_fupd f ∘ h

⊢ (∀m g f.
     m with <|carrier updated_by f; carrier updated_by g|> =
     m with carrier updated_by f ∘ g) ∧
  (∀m g f.
     m with <|op updated_by f; op updated_by g|> =
     m with op updated_by f ∘ g) ∧
  ∀m g f.
    m with <|id updated_by f; id updated_by g|> =
    m with id updated_by f ∘ g

⊢ ((∀g f. carrier_fupd f ∘ carrier_fupd g = carrier_fupd (f ∘ g)) ∧
   ∀h g f. carrier_fupd f ∘ carrier_fupd g ∘ h = carrier_fupd (f ∘ g) ∘ h) ∧
  ((∀g f. op_fupd f ∘ op_fupd g = op_fupd (f ∘ g)) ∧
   ∀h g f. op_fupd f ∘ op_fupd g ∘ h = op_fupd (f ∘ g) ∘ h) ∧
  (∀g f. id_fupd f ∘ id_fupd g = id_fupd (f ∘ g)) ∧
  ∀h g f. id_fupd f ∘ id_fupd g ∘ h = id_fupd (f ∘ g) ∘ h

⊢ ∀g. MonoidHomo I g g

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

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

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

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

⊢ ∀f g h. MonoidHomo f g h ⇒ f #e = h.id

⊢ ∀g h f.
    Monoid g ∧ MonoidHomo f g h ∧ BIJ f G h.carrier ⇒
    MonoidHomo (LINV f G) h g

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

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

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

⊢ ∀g. Monoid g ⇒ #e ∈ G

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

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

⊢ ∀g. Monoid g ⇒ #e ∈ G*

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

⊢ ∀P. (∀f f0 a. P (monoid f f0 a)) ⇒ ∀m. P m

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

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

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

⊢ ∀g h x. x ∈ (g mINTER h).carrier ⇒ x ∈ G ∧ x ∈ H

⊢ ∀g h. (g mINTER h).id = #e

⊢ ∀g h.
    (g mINTER h).carrier = G ∩ H ∧ (g mINTER h).op = $* ∧
    (g mINTER h).id = #e

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

⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G* ⇒ x ∈ G

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

⊢ ∀g. Monoid g ⇒ ∀x. x ∈ G* ⇒ |/ x ∈ G*

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

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

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

⊢ ∀g. MonoidIso I g g

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

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

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

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

⊢ ∀g h f.
    Monoid g ∧ Monoid h ∧ MonoidIso f g h ⇒
    ∀x. x ∈ G ⇒ (f x = h.id ⇔ x = #e)

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

⊢ ∀f g h. MonoidIso f g h ⇒ f #e = h.id

⊢ ∀g h f. Monoid g ∧ MonoidIso f g h ⇒ MonoidIso (LINV f G) h g

⊢ ∀g h f. Monoid g ∧ MonoidIso f g h ⇒ Monoid h

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

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

⊢ ∀g h f. Monoid g ∧ MonoidIso f g h ⇒ MonoidIso (LINV f G) h g

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

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

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

⊢ ∀f01 f1 a1 f02 f2 a2.
    <|carrier := f01; op := f1; id := a1|> =
    <|carrier := f02; op := f2; id := a2|> ⇔ f01 = f02 ∧ f1 = f2 ∧ a1 = a2

⊢ ∀m. ∃f0 f a. m = <|carrier := f0; op := f; id := a|>

⊢ ∀mm. ∃f f0 a. mm = monoid f f0 a

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

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

⊢ ∀g. Monoid 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. Monoid 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. Monoid g ⇒ ∀x. x ∈ G ⇒ ∀m. x ** m = #e ⇔ ord x divides m

⊢ ∀g. Monoid g ⇒ ∀x n. x ∈ G ⇒ (x ** n = #e ⇔ ord x divides n)

⊢ ∀g. FiniteAbelianMonoid g ⇒
      ∀x. x ∈ G ∧ 0 < ord x ⇒ ord x divides maximal_order g

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

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

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

⊢ ∀g x. Monoid g ∧ x ∈ G ∧ 0 < ord x ⇒ x ∈ G*

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

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

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

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

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

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

⊢ ∀m f0 f a.
    m with <|carrier := f0; op := f; id := a|> =
    <|carrier := f0; op := f; id := a|>

⊢ ∀f g h. Monoid g ∧ Monoid h ∧ WeakIso f g h ⇒ f #e = h.id

⊢ AbelianMonoid multiplication_monoid

⊢ Monoid multiplication_monoid

⊢ multiplication_monoid.carrier = 𝕌(:num) ∧ multiplication_monoid.op = $* ∧
  multiplication_monoid.id = 1

⊢ ∀g x.
    ord x = case OLEAST k. 0 < k ∧ x ** k = #e of NONE => 0 | SOME k => k

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

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

⊢ ∀g x. 0 < ord x ⇒ period g x (ord x)

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

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

⊢ ∀g x n. x ∈ orders g n ⇔ x ∈ G ∧ ord x = n

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

⊢ ∀g. FINITE G ⇒ ∀n. FINITE (orders g n)

⊢ ∀g n. orders g n ⊆ G

⊢ ∀n. 0 < n ⇒ AbelianMonoid (plus_mod n)

⊢ ∀n. 0 < n ⇒ ∀x k. (plus_mod n).exp x k = k * x MOD n

⊢ ∀n. FINITE (plus_mod n).carrier

⊢ ∀n. 0 < n ⇒ FiniteAbelianMonoid (plus_mod n)

⊢ ∀n. 0 < n ⇒ FiniteMonoid (plus_mod n)

⊢ ∀n. 0 < n ⇒ Monoid (plus_mod n)

⊢ ∀n. (plus_mod n).carrier = count n ∧
      (plus_mod n).op = (λi j. (i + j) MOD n) ∧ (plus_mod n).id = 0 ∧
      (∀x. x ∈ (plus_mod n).carrier ⇒ x < n) ∧
      FINITE (plus_mod n).carrier ∧ CARD (plus_mod n).carrier = n

⊢ ∀b. AbelianMonoid (power_monoid b)

⊢ ∀b. Monoid (power_monoid b)

⊢ ∀b. (power_monoid b).carrier = {b ** j | j ∈ 𝕌(:num)} ∧
      (power_monoid b).op = $* ∧ (power_monoid b).id = 1

⊢ ∀b. 1 < b ⇒ MonoidHomo (LOG b) (power_monoid b) addition_monoid

⊢ ∀b. 1 < b ⇒ MonoidIso (LOG b) (power_monoid b) addition_monoid

⊢ AbelianMonoid set_inter

⊢ Monoid set_inter

⊢ AbelianMonoid set_union

⊢ Monoid set_union

⊢ ∀g h. submonoid h g ∧ submonoid g h ⇒ MonoidIso I h g

⊢ ∀g. Monoid g ⇒
      ∀h. h << g ⇔
          H ⊆ G ∧ (∀x y. x ∈ H ∧ y ∈ H ⇒ x ∘ y ∈ H) ∧ #i ∈ H ∧ $o = $* ∧
          #i = #e

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

⊢ ∀g x. x ∈ (smbINTER g).carrier ⇔ ∀h. h << g ⇒ x ∈ H

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

⊢ ∀g. Monoid g ⇒ Monoid (smbINTER g)

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

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

⊢ ∀g. Monoid g ⇒ smbINTER g << g

⊢ ∀g. Monoid g ⇒ (smbINTER g).carrier ⊆ G

⊢ ∀g h. submonoid h g ∧ G ⊆ H ⇒ MonoidIso I h g

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

⊢ ∀g h. h << g ⇒ ∀x. x ∈ H ⇒ x ∈ G

⊢ ∀g h.
    submonoid h g ⇔ H ⊆ G ∧ (∀x y. x ∈ H ∧ y ∈ H ⇒ x ∘ y = x * y) ∧ #i = #e

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

⊢ ∀g h k f. submonoid h g ∧ MonoidHomo f g k ⇒ MonoidHomo f h k

⊢ ∀g h. h << g ⇒ Monoid h ∧ Monoid g ∧ submonoid h g

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

⊢ ∀g h k. h << g ∧ k << g ⇒ Monoid (h mINTER k)

⊢ ∀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

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

⊢ ∀g h. h << g ⇒ Monoid h

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

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

⊢ ∀g h. Monoid g ∧ Monoid h ∧ submonoid h g ⇒ ∀x. x ∈ H ⇒ order h x = ord x

⊢ ∀g h.
    h << g ⇒
    Monoid h ∧ Monoid g ∧ H ⊆ G ∧ (∀x y. x ∈ H ∧ y ∈ H ⇒ x ∘ y = x * y) ∧
    #i = #e

⊢ ∀g. submonoid g g

⊢ ∀g. Monoid g ⇒ g << g

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

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

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

⊢ ∀n. 0 < n ⇒ AbelianMonoid (times_mod n)

⊢ ∀n. (times_mod n).carrier = count n ∧
      (∀x y. (times_mod n).op x y = x * y MOD n) ∧
      (times_mod n).id = if n = 1 then 0 else 1

⊢ ∀n. 0 < n ⇒ ∀x k. (times_mod n).exp x k = (x MOD n) ** k MOD n

⊢ ∀n. FINITE (times_mod n).carrier

⊢ ∀n. 0 < n ⇒ FiniteAbelianMonoid (times_mod n)

⊢ ∀n. 0 < n ⇒ FiniteMonoid (times_mod n)

⊢ ∀n. 0 < n ⇒ Monoid (times_mod n)

⊢ ∀n. (times_mod n).carrier = count n ∧
      (times_mod n).op = (λi j. i * j MOD n) ∧
      (times_mod n).id = (if n = 1 then 0 else 1) ∧
      (∀x. x ∈ (times_mod n).carrier ⇒ x < n) ∧
      FINITE (times_mod n).carrier ∧ CARD (times_mod n).carrier = n

⊢ ∀e. FiniteAbelianMonoid (trivial_monoid e)