Email Gateway (Aug 19 2022 at 15:51): Email Gateway (Aug 19 2022 at 15:51):From: Lee Martin CCNP <tesleft@hotmail.com>
Hi
http://isabelle.in.tum.de/website-Isabelle2011/dist/library/HOL/Old_Number_Theory/Factorization.html
is it possible to do factorization mechanization for any kind of algebra?
such as semigroup, lattice, operator algebra etc.
is it possible to mechanize of construction of basis with this factorization for any kind of algebra?
Regards,
Martin
Email Gateway (Aug 19 2022 at 15:51):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
Email Gateway (Aug 19 2022 at 15:51):From: Lee Martin CCNP <tesleft@hotmail.com>
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
Email Gateway (Aug 19 2022 at 15:51):From: Lee Martin CCNP <tesleft@hotmail.com>
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
Email Gateway (Aug 19 2022 at 15:54):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi again,
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
signature.asc
Email Gateway (Aug 19 2022 at 15:54):From: Lee Martin CCNP <tesleft@hotmail.com>
Hi Florian,
Thanks. i will try to use Unique Prime Factorization first.
Regards,
Martin
Last updated: Nov 21 2024 at 12:39 UTC