*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Is factorization mechanization for any kind of algebra?*From*: Lee Martin CCNP <tesleft at hotmail.com>*Date*: Thu, 18 Sep 2014 13:20:13 +0800*Importance*: Normal*In-reply-to*: <BAY167-W69D8A26CD5751100F41C55B6B70@phx.gbl>*References*: <53E4C786.5050909@inf.ethz.ch>, , , <alpine.LNX.2.00.1408081536350.13355@lxbroy10.informatik.tu-muenchen.de>, , , , <alpine.LNX.2.00.1408091309180.35652@lxbroy10.informatik.tu-muenchen.de>, , , <53E9F7D1.9060409@inf.ethz.ch>, , , <alpine.LNX.2.00.1408131707001.27833@lxbroy10.informatik.tu-muenchen.de>, , , , <alpine.LNX.2.00.1408131723130.29642@lxbroy10.informatik.tu-muenchen.de>, , , <53EC4820.7000304@inf.ethz.ch>, , , <alpine.LNX.2.00.1408181323070.16628@lxbroy10.informatik.tu-muenchen.de>, , , <54184884.60005@inf.ethz.ch>, , <BAY167-W809370686657A4FE579B93B6B60@phx.gbl>, , <5419CAAA.2010401@informatik.tu-muenchen.de>, <BAY167-W69D8A26CD5751100F41C55B6B70@phx.gbl>

Hi Florian, 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 Regards, Martin > From: tesleft at hotmail.com > To: florian.haftmann at informatik.tu-muenchen.de; isabelle-users at cl.cam.ac.uk > Date: Thu, 18 Sep 2014 10:09:05 +0800 > Subject: Re: [isabelle] Is factorization mechanization for any kind of algebra? > > > Hi > as my understanding that algebra is the description of true of logic which called axioms > i search Unique Prime Factorization Theorem was mechanized by Boyer etc and code by Thomas Marthedal Rasmussen > Unique Prime Factorization Theorem is used to classify unique logic (axiom). > Then i think that is it possible that all kind of algebra includingnew created algebra can have Unique Prime Factorizationfor creating invariant like hilbert series to classify logic results in different combination of idealswhich means that for example, 4 polynomials, there are combinations, [1,2,3] ,[12,4],[2,3,4],[1,3,4]these ideals ideal [polynomial 1,polynomial 2, polynomial 3 ] ,[polynomial 1, polynomial 2, polynomial 4],[polynomial 2,polynomial 3, polynomial 4],[polynomial 1, polynomial 3, polynomial 4]have the same hilbert series. > Regards, > Martin > > Date: Wed, 17 Sep 2014 19:53:46 +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 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 > > >

**Follow-Ups**:**Re: [isabelle] Is factorization mechanization for any kind of algebra?***From:*Florian Haftmann

**References**:**Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing***From:*Andreas Lochbihler

**[isabelle] Is factorization mechanization for any kind of algebra?***From:*Lee Martin CCNP

**Re: [isabelle] Is factorization mechanization for any kind of algebra?***From:*Florian Haftmann

**Re: [isabelle] Is factorization mechanization for any kind of algebra?***From:*Lee Martin CCNP

- Previous by Date: Re: [isabelle] PolyML "Insufficient memory" exception while building images
- Next by Date: Re: [isabelle] PolyML "Insufficient memory" exception while building images
- Previous by Thread: Re: [isabelle] Is factorization mechanization for any kind of algebra?
- Next by Thread: Re: [isabelle] Is factorization mechanization for any kind of algebra?
- Cl-isabelle-users September 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list