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.

## Advertising

Mario On Tue, Jul 19, 2016 at 6:24 AM, Manuel Eberl <ebe...@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-...@in.tum.de >>> >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>> >>> >> >> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> >> _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >

_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev