[isabelle-dev] multiplicity and prime numbers

[Mario Carneiro]

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.

Mario

On Tue, Jul 19, 2016 at 6:24 AM, Manuel Eberl <eberlm at in.tum.de> wrote:

> 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?
>
> 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.
>
> 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.
>
>
> Cheers,
>
> Manuel
>
>
>
> On 19/07/16 12:18, Tobias Nipkow wrote:
>
>> Are you sure that there is no standard definition of this concept in
>> mathematics that we should follow?
>>
>> Tobias
>>
>> On 19/07/2016 12:03, Manuel Eberl wrote:
>>
>>> Hallo,
>>>
>>> as some of you may already know, I am currently in the process of
>>> resructing
>>> Isabelle's definitions of prime numbers. Before these changes, we had the
>>> concept of "multiplicity". This was defined to be the multiplicity of
>>> a prime
>>> factor in the prime decomposition of a natural number or an integer. The
>>> multiplicity of a non-prime was defined to be 0.
>>>
>>> I have now created an alternative definition of "multiplicity" which
>>> is simply
>>> defined as "the highest power that is still a divisor" (as long as
>>> this is
>>> well-defined); e.g. the multiplicity of -4 in 64 would be 3.
>>>
>>> I see three possibilities:
>>> 1. redefine my "new", more general multiplicity to the "old" multiplicity
>>> 2. keep both notions of multiplicity around with different names
>>> 3. replace the old multilicity with the new one and adapt all lemmas
>>> accordingly
>>>
>>> Currently, I tend towards the last options. Are there any other
>>> opinions on this?
>>>
>>>
>>> Cheers,
>>>
>>> Manuel
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>>
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>>
>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>>
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160719/0daf1c40/attachment-0002.html>