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.`

## Advertising

`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