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.



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?


On 19/07/2016 12:03, Manuel Eberl wrote:

as some of you may already know, I am currently in the process of
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

Currently, I tend towards the last options. Are there any other
opinions on this?


isabelle-dev mailing list

isabelle-dev mailing list

isabelle-dev mailing list

Reply via email to