[isabelle-dev] multiplicity and prime numbers

[Manuel Eberl]

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
>