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