---

Step * of Lemma unique_mfact

∀g:IAbMonoid
  (Cancel(|g|;|g|;*) ⇒ (∀a,b:|g|.  Dec(a | b)) ⇒ (∀ps,qs:Prime(g) List.  (((Π ps) ~ (Π qs)) ⇒ ps ≡ qs upto ~)))
BY
{ TACTIC:(InductionOnListA THEN All Reduce THEN Auto) }

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

2
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. ∀a,b:|g|.  Dec(a | b)
4. p : Prime(g)
5. ps : Prime(g) List
6. ∀qs:Prime(g) List. (((Π ps) ~ (Π qs)) ⇒ ps ≡ qs upto ~)
7. qs : Prime(g) List
8. (p * (Π ps)) ~ (Π
                    qs)
⊢ [p / ps] ≡ qs upto ~

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid
    (Cancel(|g|;|g|;*)
    {}\mRightarrow{}  (\mforall{}a,b:|g|.    Dec(a  |  b))
    {}\mRightarrow{}  (\mforall{}ps,qs:Prime(g)  List.    (((\mPi{}  ps)  \msim{}  (\mPi{}  qs))  {}\mRightarrow{}  ps  \mequiv{}  qs  upto  \msim{})))


By

---

Latex:
TACTIC:(InductionOnListA  THEN  All  Reduce  THEN  Auto)

---

Home Index