---

Step * 1 of Lemma unique_mfact


1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. ∀a,b:|g|.  Dec(a | b)
4. qs : Prime(g) List
5. e ~ (Π
         qs)
⊢ [] ≡ qs upto ~
BY
{ TACTIC:D 5 THEN Thin 5  THEN FoldTop `munit` 5 }

1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. ∀a,b:|g|.  Dec(a | b)
4. qs : Prime(g) List
5. g-unit(Π
           qs)
⊢ [] ≡ qs upto ~

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  Cancel(|g|;|g|;*)
3.  \mforall{}a,b:|g|.    Dec(a  |  b)
4.  qs  :  Prime(g)  List
5.  e  \msim{}  (\mPi{}
                  qs)
\mvdash{}  []  \mequiv{}  qs  upto  \msim{}


By

---

Latex:
TACTIC:D  5  THEN  Thin  5    THEN  FoldTop  `munit`  5

---

Home Index