But is it possible to adapt all lemmas accordingly? I could imagine
that some statements use the fact that the support of multiplicity are
the prime numbers.
Not really. Some facts will still require the primality assumption, e.g.
lemma prime_multiplicity_mult_distrib:
assumes "is_prime_elem
I also would vote for option 3.
But is it possible to adapt all lemmas accordingly? I could imagine
that some statements use the fact that the support of multiplicity are
the prime numbers.
- Johannes
Am Dienstag, den 19.07.2016, 12:09 +0100 schrieb Lawrence Paulson:
> This is what I would do
The reason why we put x/0= 0 is because it simplifies the statements of many
laws, not because of any admiration of 0.
Larry
> On 19 Jul 2016, at 11:24, Manuel Eberl <ebe...@in.tum.de> wrote:
>
> The obvious possibility would be to just let all non-prime numbers have
&
This is what I would do
Larry Paulson
> On 19 Jul 2016, at 11:03, Manuel Eberl wrote:
>
> 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?
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.
Mario
On Tue, Jul 19, 2016 at 6:24 AM, Manuel Eberl wrote:
> As far as I know,
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
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
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