---

Step * 1 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. g-unit(Π
           qs)
⊢ [] ≡ qs upto ~
BY
{ TACTIC:(D 4 THEN All Reduce) }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(D  4  THEN  All  Reduce)

---

Home Index