[isabelle-dev] multiplicity and prime numbers

[Tobias Nipkow]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160719/4a729ace/attachment.bin>