nat.prime

Stream: general

[Johan Commelin]

We have docs#nat.prime and docs#prime. Should we redefine nat.prime in terms of _root_.prime?

[Johan Commelin]

cc @Stuart Presnell , because you've been working with nat.prime a lot recently.

[Eric Wieser]

Do we even have the statement that the two notions are equivalent?

[Mario Carneiro]

pretty sure

[Mario Carneiro]

docs#nat.prime_iff

[Mario Carneiro]

Although, there is both irreducible and prime and neither one is a clear winner for the definition of nat.prime

[Mario Carneiro]

I worry about dependency bloat, of course. It would be nice to make these kinds of things quantitative, for example, calculating the sum of the depths of all files before and after

[Anne Baanen]

If we can split off the big_operators dependency from algebra.associated, the remainder is low-level definitions such as group_with_zero and units. So I'm in favour of unifying nat.prime with _root_.prime after such a split.

[Johan Commelin]

Right, clearly big_ops shouldn't be a dependency.

[Johan Commelin]

But otherwise, I think it's quite mild.

[Eric Wieser]

Mario Carneiro said:

I worry about dependency bloat, of course. It would be nice to make these kinds of things quantitative, for example, calculating the sum of the depths of all files before and after

Do the stats at https://eric-wieser.github.io/mathlib-import-graph/?highlight=mathlib%3Aring_theory.int.basic help? If you hover over the highlighted node, it tells you that 31285 declarations appear before that file, and 248 files consume it.

[Ruben Van de Velde]

Oh, I think I broke that dependency at some point, but then didn't land that? It's just exists_mem_finset_dvd that needs it

[Ruben Van de Velde]

That was in #9606 - that lemma isn't even used in mathlib

[Floris van Doorn]

I am strongly in favor of removing nat.prime and just using prime everywhere.

[Kevin Buzzard]

I guess p.prime is no shorter than prime p.

[Johan Commelin]

That's not the point. The point is deduplicating all the lemmas.

[Anne Baanen]

Step 1: #10848

[Ruben Van de Velde]

I started looking into this at branch#nat-prime-irreducible - I tried with prime, but it seems like the nat.prime <-> prime equivalence requires a fair amount of material. irreducible is essentially the current definition, so that seems to work better to build up the api.

(Code is still a mess at this point)

[Johan Commelin]

Thanks for taking this up!

[Ruben Van de Velde]

To my surprise, I seem to have made it back to a compiling mathlib with +108-105 changes

[Ruben Van de Velde]

#11031

[Johan Commelin]

Thanks!

[Johan Commelin]

@Mario Carneiro Are you happy with this new state of affairs? It looks good to me

[Mario Carneiro]

Looks good, it looks like imports weren't affected too much

[Johan Commelin]

I think it is confusing that nat.min_fac_prime does not make progress on prime (nat.min_fac N).