<div dir="ltr"><div>FWIW I can attest to your "new" definition being the standard one in Metamath. It also avoids any a priori notion of primality, which allows it to apply in more general circumstances.<br><br></div>Mario<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jul 19, 2016 at 6:24 AM, Manuel Eberl <span dir="ltr"><<a href="mailto:eberlm@in.tum.de" target="_blank">eberlm@in.tum.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">As far as I know, ‘multiplicity’ in mathematics is only defined for prime factors. That is a luxury that we do not have in HOL, so the question is: How do we extend the definition to the full domain?<br>
<br>
The obvious possibility would be to just let all non-prime numbers have multiplicity 0. This makes a few things look nicer (e.g. the prime factors are then precisely the numbers with non-zero multiplicity). However, it also means that the multiplicity of "X - 1" in "X² - 1" is 1, whereas the multiplicity of "1 - X" is 0, which I find a bit odd.<br>
<br>
A more general possibility is that which I chose, i.e. the biggest n such that p^n divides x. This is well-defined as long as x is non-zero and p is not a unit. I would argue that having a more general notion like this is nicer.<br>
<br>
<br>
Cheers,<br>
<br>
Manuel<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
On 19/07/16 12:18, Tobias Nipkow wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Are you sure that there is no standard definition of this concept in<br>
mathematics that we should follow?<br>
<br>
Tobias<br>
<br>
On 19/07/2016 12:03, Manuel Eberl wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hallo,<br>
<br>
as some of you may already know, I am currently in the process of<br>
resructing<br>
Isabelle's definitions of prime numbers. Before these changes, we had the<br>
concept of "multiplicity". This was defined to be the multiplicity of<br>
a prime<br>
factor in the prime decomposition of a natural number or an integer. The<br>
multiplicity of a non-prime was defined to be 0.<br>
<br>
I have now created an alternative definition of "multiplicity" which<br>
is simply<br>
defined as "the highest power that is still a divisor" (as long as<br>
this is<br>
well-defined); e.g. the multiplicity of -4 in 64 would be 3.<br>
<br>
I see three possibilities:<br>
1. redefine my "new", more general multiplicity to the "old" multiplicity<br>
2. keep both notions of multiplicity around with different names<br>
3. replace the old multilicity with the new one and adapt all lemmas<br>
accordingly<br>
<br>
Currently, I tend towards the last options. Are there any other<br>
opinions on this?<br>
<br>
<br>
Cheers,<br>
<br>
Manuel<br>
_______________________________________________<br>
isabelle-dev mailing list<br>
<a href="mailto:isabelle-dev@in.tum.de" target="_blank">isabelle-dev@in.tum.de</a><br>
<a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" rel="noreferrer" target="_blank">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br>
<br>
</blockquote>
<br>
<br>
<br>
_______________________________________________<br>
isabelle-dev mailing list<br>
<a href="mailto:isabelle-dev@in.tum.de" target="_blank">isabelle-dev@in.tum.de</a><br>
<a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" rel="noreferrer" target="_blank">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br>
<br>
</blockquote>
_______________________________________________<br>
isabelle-dev mailing list<br>
<a href="mailto:isabelle-dev@in.tum.de" target="_blank">isabelle-dev@in.tum.de</a><br>
<a href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev" rel="noreferrer" target="_blank">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a><br>
</div></div></blockquote></div><br></div>