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



Hi Martin,

On 17.09.2014 08:19, Lee Martin CCNP wrote:
> http://isabelle.in.tum.de/website-Isabelle2011/dist/library/HOL/Old_Number_Theory/Factorization.html

this is an odd location. The current Isabelle release is Isabelle2014. A
suitable entrance point would be
http://isabelle.in.tum.de/dist/library/HOL/HOL-Number_Theory/UniqueFactorization.html

> is it possible to do factorization mechanization for any kind of algebra?
> such as semigroup, lattice, operator algebra etc.

According to my understanding factorization has something to do with
divisibility and factors and makes only sense for rings. What do you
mean by »mechanization«? Computation?

Can you provide some clues what you want to achieve by giving references
to articles or explaining in more detail?

Cheers,
	Florian


> is it possible to mechanize of construction of basis with this factorization for any kind of algebra?
> Regards,
> Martin 		 	   		  
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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