Re: [isabelle] Is factorization mechanization for any kind of algebra?



Hi Florian,
Thanks. i will try to use Unique Prime Factorization first.
Regards,
Martin
> Date: Thu, 25 Sep 2014 10:37:02 +0200
> From: florian.haftmann at informatik.tu-muenchen.de
> To: tesleft at hotmail.com; isabelle-users at cl.cam.ac.uk
> Subject: Re: [isabelle] Is factorization mechanization for any kind of	algebra?
> 
> Hi again,
> 
> > In another words, create invariant like hilbert series can classify ideals and matrix groups into different axioms.
> > each axioms is like a Unique Prime Factorization.
> > so is it possible to mechanize Unique Prime Factorization for different algebra and then classify these algebra's ideals or matrix group into axioms
> 
> well, since it seems to be a mathematical concept, you can surely
> *formalize* it.  Since it seems to be an advanced topic were little has
> been done so far in Isabelle/HOL, it will require a considerable amount
> of work and is definitely nothing which I would recommend to start
> without prior experience in Isabelle/HOL.
> 
> Cheers,
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.